Notation:

Notation:

Notation: Q : formal system (logical & nonlogical axioms, etc.) of Robinson's arithmetic; wff : well formed formula; |- : proves. G1IT is always stated in the form: If Q is consistent then exists wff x: ¬(Q |- x) & ¬(Q |- ¬x) but we cannot prove it within Q (simply because there is no deduction rule to say "Q doesn't prove" (there is only modus ponens and generalization)), so it's incomplete statement, I don't see WHERE (in which formal system) IS IT STATED. (Math logic is a formal system too.) In my opinion, some correct answer is to state the theorem within a copy of Q: Q |- Con(O) |- exists x ((x is wff of O) & ¬(O |- x) & ¬(O |- ¬x)) where O is a copy of Q inside Q, e.g. ¬(O |- x) is an arithmetic formula of Q, Con(O) means contradiction isn't provable...such formulas can be constructed (see Godel's proof). But I'm confused because I haven't found such statement (or explanation) anywhere. Thank You Very Much

Read another response by Peter Smith, Richard Heck
Read another response about Logic
Print