*Post by peteolcott*I don't know why you think the most direct formalization of "this sentence is not true" should end up as "for every proposition, truth is logically equivalent to unprovability".

The above poor paraphrase

Because of the high quality of your reviews, I always make sure to provide

a precisely accurate response even if I have to reread them after I have responded.

Upon further review your "error" may have been nothing more than using a simpler

term so that communication would be more effective.

"it says that every single proposition is materially equivalent to a statement of its own unprovability."

The only thing that you got wrong is the distinction between Provability and Theoremhood.

Since my reasoning applies to both Provability and Theoremhood your error is not significant.

It probably just seemed too unconventional and weird to say untheoremhood instead of unprovability.

I have to keep quoting this because "valid" has a distinctly different meaning

within the context of symbolic logic:

Validity and Soundness https://www.iep.utm.edu/val-snd/

A deductive argument is said to be valid if and only if it takes a form that makes it

impossible for the premises to be true and the conclusion nevertheless to be false.

Otherwise, a deductive argument is said to be invalid.

A deductive argument is sound if and only if it is both valid, and all of its premises

are actually true. Otherwise, a deductive argument is unsound.

The following shows the mapping between (syntax/provability) and

(semantics/logical deduction) without any separate set of notational conventions:

An argument is provable (valid) Γ ⊢ X even if its premises are false.

An argument is a theorem (sound) ⊢X only if it has no (false) premises

*Post by peteolcott*For all LP, LP is logically equivalent to ~⊢LP

How do you think they're different?

*Post by peteolcott*You are correct that the universal quantifier is not apt.

∃x (x ↔ ~True(x))

∃x (x ↔ ~Theorem(x))

∃x (x ↔ ~⊢x )

Nope, this still doesn't do what you want. The second and third version will be true if there is some proposition somewhere that is true but not provable, which is exactly what Gödel says.

Paraphrase of your prior words:

"it says that THERE EXISTS a proposition is materially equivalent to a statement of its own unprovability."

https://plato.stanford.edu/entries/goedel-incompleteness/#FirIncTheCom

(G) F ⊢ GF ↔ ~ProvF(⌈GF⌉)

simplified to

(G) F ⊢ GF ↔ ~ProvF(GF)

simplified to

G ↔ ~Provable(G)

add existential quantifier

∃G (G ↔ ~Provable(G))

Paraphrase of your prior words:

"it says that THERE EXISTS a proposition is materially equivalent to a statement of its own unprovability."

If G was Provable this contradicts its assertion: G is not Provable.

If ~G was Provable this contradicts its assertion: G is Provable

∴ ~Logic_Sentence(G)

Copyright 2018 Pete Olcott

Once we strip off the tiny bit of remaining extraneous complexity from

the (Raatikainen fall2018) enormous simplifications, we simply have the

above refutable expression of formal language.

(Raatikainen fall2018)

Raatikainen, Panu, "Gödel's Incompleteness Theorems", The Stanford

Encyclopedia of Philosophy (Fall 2018 Edition), Edward N. Zalta (ed.),

URL = <https://plato.stanford.edu/archives/fall2018/entries/goedel-incompleteness/>.

Nothing in your formalization captures the notion of "this sentence", which is a crucial part of the liar's paradox (the other crucial part if a truth predicate, which isn't just a relabelling of ⊢). You need self-reference, which doesn't exist in standard logic, so you can't just do your usual combination of a random mess of existing logical symbols and hope it leads to self-reference.

EFQ

You need self-reference, which doesn't exist in standard logic,

I don't know why you think the most direct formalization of "this sentence is not true" should end up as

"for every proposition, truth is logically equivalent to unprovability".