# How to give formal proof in logic?

I am taking a course on mathematical logic and am struggling to give formal proofs of theorems or claims. Currently doing first order logic. Here, an example:

Claim: $$\models (\exists x)\big(A(x)\Rightarrow (\forall y)(A(y))\big)$$

where $$A$$ is an unary predicate. I am asked to prove this. This is how I would reason:

By the rule of propositional logic $$P\Rightarrow Q$$ is equivallent to $$\neg P\vee Q$$. So we wish to show that $$\models(\exists x)\big(\neg A(x)\vee (\forall y)(A(y))\big)$$ So, assume we have an arbitrary interpretation of language $$\mathcal{L}=\{A\}$$, that is a nonempty set $$M$$ together with unary predicate $$A$$.. By Tarski's definition of truth, there is some $$m\in M$$ for which is $$\neg A(m)$$ or for all $$n\in M$$ $$A(n)$$ holds. But this is clearly true (logically valid). Because whenever there is some $$m\in M$$ for which $$\neg A(m)$$, then the formula is satisfied. If not, then for all $$n\in M$$ for which $$A(n)$$, which makes it also satisfied.

Now, I am wondering whether this can be taken as a formal proof of the claim that the formula is logically valid in any interpretation of the language $$\mathcal{L}=\{A\}$$. It seems really trivial, but I am afraid I am using too much of set theory.

Another reasoning could be: In fact, when $$A$$ is an unary predicate, that means $$A$$ is a subset of $$M$$. Now distinguish two cases: 1. $$A=M$$, then $$(\forall y)((y\in M) \Leftrightarrow (y\in A))$$ in other words $$(\forall y)(A(y))$$. If $$A\subsetneq M$$ then it is clear there is some $$m\in M$$ that is not in $$A$$, in this case the part $$(\exists x)(\neg A(x))$$ is true. Now, this uses the definition of equality between sets and what is a subset.

Another idea: Using a contradiction. Assume this was not logically valid, so there exists some interpretation $$\mathcal{M}$$ and value assignment $$e$$ for which $$\mathcal{M}\models \neg(\exists x)\big(A(x)\Rightarrow (\forall y)(A(y))\big)$$, that is $$\mathcal{M}\models(\forall x)(A(x)\wedge (\exists y)(\neg A(y))$$, thus for all $$m$$ $$\mathcal{M}\models A(m)\wedge (\exists y)(\neg A(y))$$, by definition again there is some $$n\in M$$ for which $$\mathcal{M}\models A(m)\wedge \neg A(n)$$, this gives $$\mathcal{M}\models A(n)$$ (the $$n$$ must be one of all of the $$m$$'s) but also $$\mathcal{M}\models \neg A(n)$$. Which is contradiction by the law of excluded middle, so the statement before was logically valid.

Or just by looking: It is clear that either for all $$x$$ $$A(x)$$ holds, or there is some $$x$$ for which $$A(x)$$ doesn't hold...

All this seems like a handwaving...

So, what tools/methods/kind of reasoning should I use at most when proving such claims and theorems in logic/model theory? I would be grateful for opinions and/or more examples (sources).

• The first proof is correct and very easy to follow; thus, IMO, is good. You can "merge" 1 and 2 avoiding the propositional transromation and consider the two cases directly in 1 : either (i) all $m \in M$ are $A$s (in which case the conditional has True consequent and is True), or there is some $m_0 \in M$ that is not $A$ (in which case the conditional is False $\to$ False and thsu True for it). – Mauro ALLEGRANZA Dec 27 '18 at 13:12

Your proof is correct. You used the mathematical definitions of all the terms involved, like "valid", "interpretation", and "true in an interpretation" and came up with a rigorous argument that the statement was in fact valid according to those definitions.

People often are under the mistaken impression that just cause we're studying logic, we need to stop being mathematicians and turn into C++ compilers. (Mathematical) logic is a branch of mathematics like any other, where we argue informally$$^*$$ but rigorously about mathematical constructions. It's just that in the case of logic, our arguments are often about formal proofs, which are themselves mathematical constructions. However, in a certain sense, the whole point of semantics and model theory is to eschew formal proofs and to instead think about sentences in their 'plain meaning' within mathematical structures they might talk about.

Semantics do require stronger philosophical precepts than syntactical proofs (as you allude to, there is some set theory involved). You could also construct a formal proof of your statement in some proof calculus for first order logic, and such a construction would only involve finitary ideas. If we do this we would say that $$\vdash (\exists x)\big(\neg A(x)\vee (\forall y)(A(y))\big)$$ (with a $$\vdash$$ meaning "provable (in some given deductive system)" rather than a $$\models$$ meaning "valid").

Remarkably, the standard proof systems for first order logic are complete and sound, i.e. they can prove a sentence if and only if it is semantically valid, i.e. $$\vdash \phi\iff \models\phi$$. While formal proofs are less of a philosophical burden, as a practical matter it is generally harder to construct formal proofs than to make semantic arguments. But formal proofs are very important philosophically, especially if you're worried about foundational matters. They are also interesting objects of study in their own right. (And the notion that “true in all models” and “effectively provable in a formal system” are equivalent is particular to first order logic, anyway.)

$$^*$$Here we might have a clash of terminology between the way you’re using the term "formal" vs the way logicians typically use the term. To a logician, a formal proof of a logical sentence is a mathematical object constructed according to some formal mathematical rules for proof construction. A rigorous natural language argument that a certain mathematical statement is true is an informal proof, regardless of how water-tight and well-explained the reasoning is. (Although you will still hear logicians occasionally use 'formal' to mean 'careful / detailed / rigorous'). Formal proofs are meant as models of well-reasoned arguments, and of course the more careful / detailed / rigorous - ly an informal proof is phrased, the easier it is to imagine it being translated into a formal proof in some suitable system.

• Thanks for nice explanation. True, I quite mixed up the terms. In my case, I am not actually looking for the formal proof as a sequence of formulas beginning from axioms and applying interference rules etc. I was just wondering, if I can be more rigorous or if there is something more behind my reasoning. All the way throughout logic and these definitions of truth seem really circular to me. Say $\mathcal{M}\models \forall x\varphi [e]$ if for any $m\in M$ $\mathcal{M}\models \varphi[e(x/m)]$.... – Michal Dvořák Dec 28 '18 at 0:22
• @Michal Well, your argument was rigorous enough for me. I think you’ll find if you think about it long enough is that it is not circular at all. What it is is obvious. Tarski’s famous phrase was “‘Snow is white’ is true if and only if snow is white.” How would you assess the meaning of the sentence $\exists x(x^2=2)$? First you’d ask what the sentence is supposed to be about. Say it’s the real numbers. Then you’d assess whether there is some real number that squares to $2.$ It’s a very simple process that can be afforded an obvious mathematical description. – spaceisdarkgreen Dec 28 '18 at 1:02
• Think about it this way: you are taking a meaningless sequence of symbols and giving them a meaning (by interpreting them in a structure). $\exists x\phi(x)$ should mean no more and no less than “there is a $a$ in the domain such that $\phi(x/a)$ is true.” First order logic is a language we associate naturally with making statements about structures with definite truth values. – spaceisdarkgreen Dec 28 '18 at 1:08
• However the simplicity in this special case (which is generally the first and perhaps only kind of semantics people learn other than truth tables) is misleading. There are many ways to attach mathematical objects to sentences other than just a binary true or false (even within the confines of classical first order logic) and many other different types of logic that require more mathematically sophisticated types of semantics to study. – spaceisdarkgreen Dec 28 '18 at 1:22
• Thanks for your words, I think I have better idea about it now =) – Michal Dvořák Dec 28 '18 at 4:31