blegging for logic help

[gusl]

Since I'm supposed to know something about logic once I graduate, I'm trying some self-study and talking to people who know more than me. All this extra-curricular.

Any help clarifying my ideas is very welcome!


Here are some notes:

ZFC talks about sets
PA talks about numbers
you can code PA into ZFC
Goodstein theorem is undecidable in PA
Goodstein theorem is provable in ZFC


Is there a relationship between the Undecidability of FOL and Gödel's incompleteness?


Are these the same meaning of "complete"?
complete: all tautologies are provable
complete: all consistent things have a model


What can one conclude from "FOL is complete but not decidable"?



What's the relationship between:

calculus
logic
theory
?

logic = calculus + semantics?

---

I really should be ashamed of myself, but it really seems I can't learn from a static book (possibly because I don't have the patience!). But I have an open mind: perhaps I just haven't found the right book.

Comments

[easwaran.livejournal.com]

I don't know of any ways to prove the undecidability of FOL without using Godel's Incompleteness theorems, or the halting problem, or something equivalent. I don't know if there's a stronger connection than that.

All tautologies being provable and every consistent set of formulas having a model are equivalent results, given the deduction theorem and reductio (these are simple metatheorems of first order logic). Assume that every consistent set of formulas has a model. Now assume that a formula is not provable. Then the singleton consisting of its negation is consistent, because otherwise you could prove the formula (by reductio). So there is a model for the negation of the formula, so the formula is not a tautology. These steps work in reverse order as well.

Being complete means that every consistent set has a model. Not being decidable means that there is no syntactic procedure for validity checking. I think together these basically mean that there's no syntactic check for model equivalence. (Lowenheim-Skolem implies that there are non-isomorphic models that are elementarily equivalent, incompleteness just implies that there are non-equivalent models satisfying any recursive set of formulas.)

[gustavolacerda.livejournal.com]

Thank you.

I would like to see how the undecidability of FOL follows from Godel's incompleteness.

[easwaran.livejournal.com]

If there were a decision procedure for FOL, then because PA is recursively axiomatizable, there would be a decision procedure for PA. Using this decision procedure, we could create a recursive set of axioms that decide all formulas in the language by enumerating all formulas in some uniform way, determining whether or not they follow from the axioms of PA and whatever other axioms have been added earlier in the procedure, and adding the formula as an axiom if neither it nor its negation follows from the previous axioms (which is decidable by the decision procedure and the fact that the set of axioms at any moment is recursive). Thus, if the consequence relation for FOL were decidable, we could get a recursively axiomatizable extension of PA that decided all formulas, which would contradict Godel's theorem.