First Order Logic and an ontological argument

[I also posted this on prosblogion.]

I want to give this argument in part to provoke a bit of discussion of the role of FOL in philosophy. I don't think the argument carries great weight, in large part because of Objection 2 (see the end).

1. (Premise) The inferences allowed by classical First Order Logic (FOL) combined with a modal logic that includes Necessitation are valid.
2. (Premise) If every being is contingent, then possibly nothing exists. (A material conditional)
3. Necessarily something exists. (By 1)
4. So, there is a necessary being. (By 2 and 3)

The proof of (3) is as follows. Classical logic allows (Ex)(x=x) to be inferred from (x)(x=x). Since (x)(x=x) is a theorem, so is (Ex)(x=x), and hence by the rule of Necessitation, we have: Necessarily (Ex)(x=x). And thus (3) follows. And of course Necessitation is a part of standard modal systems like M, S4 and S5.

I think (2) is intuitively plausible. Here is one way to try to argue for it:
5. (Premise for reductio) Premise (2) is false.
6. (Premise) The non-existence of non-unicorns does not necessitate the existence of unicorns.
7. Every being is contingent and it is necessary that at least one thing exists. (By 5)
8. Necessarily, if no non-unicorns exist, then at least one thing exists. (By 7)
9. Necessarily, if no non-unicorns exist, then at least one unicorn exists. (By 8) 
Since (9) contradicts (6), our reductio argument for premise (2) is complete.

(I am grateful to Josh Rasmussen for simplifying my original argument.)

Now, the weak point in the argument, I think, is premise 1, and specifically the assumption of classical FOL which allows the derivation of (Ex)F(x) from (x)F(x). In a free logic, this wouldn't happen.

But it is still an interesting fact, and a real cost to contingentism (the view that all beings are contingent), that it requires one to abandon classical logic or modify Necessitation. After all, there is some non-negligible prior probability that classical logic and Necessitation license only valid inferences.

Moreover, there is the question of why one should go for a free logic? If one's reason for going for a free logic is precisely that FOL licenses the derivation of (Ex)F(x) from (x)F(x), then one runs the danger of begging the question against the anti-contingentist, in that the derivation is valid (in the sense that necessarily if the premise is true, so is the conclusion) if there is a necessary being.

Objection 1: There is likewise a cost to the non-contingentist who is prevented from adopting those logics on which it is provable that possibly nothing exists.

Response: The non-contingentist who accepts such a logic can still make the move of distinguishing metaphysical and narrowly logical necessity. She can then say that the logic gives an account of narrowly logical necessity. Therefore, all that is shown in such a logic is that it is narrowly logically possible that nothing exists, but not that it is metaphysically possible that nothing exists. On the other hand, it is much harder for the contingentist to make the analogous move of saying that (3) is true in the case of "narrowly logical necessity". For it is widely accepted that if there is a distinction between metaphysical and narrowly logical necessity, the narrowly logical necessity is stronger of the two. Thus, if one accepts (3) with "narrowly logical necessity", one accepts (3) with metaphysical necessity, too.

Objection 2: There are other good reasons to accept free logic, besides the fact that FOL licenses the derivation of (Ex)F(x) from (x)F(x). Specifically, FOL+Necessitation implies that:
10. Necessarily (Ex)(x=a)
is true for every name a.

Response: This objection almost convinces me and is one of the main reasons why I think that while my argument lowers the probability of contingentism, it is not very powerful.

I do think there are two speculative responses to the objection, which is why I think my argument still has some weight.

i. The truth of (10) for every "name" a shows that FOL's "names" do not correspond in function to names in natural languages. In particular, they show that when translating natural language sentences into FOL, one can only employ FOL's "names" for necessary beings. This shows a significant limitation of FOL--namely, that FOL has no way of translating sentences like "Socrates is mortal." However, the fact that a logic has no way of translating a sentence does not mean that the logic's inferences are invalid. There is probably no standard formal logic that can translate all sentences of natural language.

ii. Another move in defense of FOL+Necessitation is that we should see the inclusion of non-dummy names in a language L as embodying existential assumptions about the referents of these names. Consequently, when we give the Tarskian semantics for a modal logic built on top of FOL, the recursive clauses for "Necessarily s" and "Possibly s" in a language L under an interpretation J should respectively read:
- Necessarily: If e(L,J), then s.
- Possibly: e(L,J) and s.
Here, e(J,L) is the conjunction of all metalanguage claims of the form "a* exists" where "a*" is a metalanguage name for the entity that the L-name "a" refers to under J, if L contains any names, and is any tautology otherwise. Then my initial argument needs to be run in a language with no names.

Propositional logic

I am now teaching Fitch-style propositional logic proofs with and, or and not. I had some fun last night and wrote a fun little proof generator in perl (or, perhaps more precisely, modperl). This morning I'm going to teach the students the simple brute-force method that the code uses (basically, just go through all the possible combinations of truth values), which I assume is pretty standard. While the method tends to generate proofs that are unduly long, I think there is a value in having a method that is guaranteed to work even if one is suffering from prover's block. Besides, the algorithm makes it intuitively clear why truth-table completeness holds for propositional logic.

I was going to post a link to a web service that runs the prover. But I then thought that a student at another institution might cheat with it (even though the proofs generated have a somewhat identifiable look, and there is always the risk of bugs in my code), and so I didn't do it. If you're a faculty member, or are someone I know and trust, and are curious to see the code run, email me and I might send you a private link. Of course, someone determined on cheating can use the source code that I posted, but I bet there is other source code posted online that does things like that.

[The code in the link continues to evolve. For instance, it now does some easy simplifications optionally. - Note added later]