Conclusion

So, which logic is superior? It depends to some extent on what we need it for. Anything provable in first order logic can be proved in second order logic, so if we have a choice of proofs, picking the first order one is the better option. First order logic has more pleasing internal properties, such as the completeness theorem, and one can preserve this in second order via Henkin semantics without losing the ability to formally express certain properties. Finally, one needs to make use of set theory and semantics to define full second order logic, while first order logic (and Henkin semantics) get away with pure syntax.

On the other hand, first order logic is completely incapable of controlling its infinite models, as they multiply, uncountable and generally incomprehensible. If rather that looking at the logic internally, we have a particular model in mind, we have to use second order logic for that. If we’d prefer not to use infinitely many axioms to express a simple idea, second-order logic is for us. And if we really want to properly express ideas like “every set has a least element”, “every analytic function is uniquely defined by its power series” – and not just express them, but have them mean what we want them to mean – then full second order logic is essential.

— Completeness, incompleteness, and what it all means: first versus second order logic

— Stuart Armstrong

2014.01.11 Saturday ACHK

A monoid is a set with an associative binary operation that has an identity element. By the same technique as for groups, any monoid “is” a category with exactly one object and any category with exactly one object “is” a monoid.

— Wikibooks on Category Theory/Categories

2014.01.08 Wednesday ACHK

Theorem 1.

Propositional logic is sound with respect to truth-value semantics.

Proof.

Basically, we need to show that every axiom is a tautology, and that the inference rule modus ponens preserves truth. Since theorems are deduced from axioms and by applications of modus ponens, they are tautologies as a result.

— truth-value semantics for propositional logic is sound

— PlanetMath

2013.12.15 Sunday ACHK

The truth of the Godel sentence

The proof of Godel’s incompleteness theorem just sketched is proof-theoretic (also called syntactic) in that it shows that if certain proofs exist (a proof of P(G(P)) or its negation) then they can be manipulated to produce a proof of a contradiction. This makes no appeal to whether P(G(P)) is “true”, only to whether it is provable. Truth is a model-theoretic, or semantic, concept, and is not equivalent to provability except in special cases.

By analyzing the situation of the above proof in more detail, it is possible to obtain a conclusion about the truth of P(G(P)) in the standard model (\mathbb{N}) of natural numbers. As just seen, q(n,G(P)) is provable for each natural number n, and is thus true in the model (\mathbb{N}). Therefore, within this model,

P(G(P)) = \forall y\, q(y,G(P))

holds. This is what the statement “P(G(P)) is true” usually refers to — the sentence is true in the intended model. It is not true in every model, however: If it were, then by Godel’s completeness theorem it would be provable, which we have just seen is not the case.

— Wikipedia on Proof sketch for Godel’s first incompleteness theorem

2013.11.14 Thursday ACHK