Tarski's theorem

An axiom must show independance from the framework it supports?

File: all dose people all dose hamboigahs.jpg (69KB, 468x683px) Image search: [Google]

69KB, 468x683px

>>7784987
The proof system is undecidable, only recognizable (in terms of false statements). In other words you can test whether a statement is false (in finite time) by using an algorithm that will eventually find a counterexample for it. However, the same algorithm will never terminate when given a true statement (because it will just keep searching for a counterexample until the end of time). Unfortunately there is no algorithm for checking if a statement is true, which intuitively makes sense. Consider the statement
>All cheeseburgers that will ever exist will taste good.
In order to test this you would need to check every cheeseburger (granted one could argue that in a finite universe there will exist a finite number of burgers, but that would be missing the point). Hence you can test if a statement is true but you cannot test if a statement is false. This means you can't define a predicate for truth. More importantly it means that the problem of falsehood is not decidable but it is recognizable.

Pic related.

>>7785014
>This means you can't define a predicate for truth.
can you detail this ?
to me a predicate is just written P(x) with x some variable and P some shorthand for a sentence. then in set theory, a predicate is a subset and x a pint of the universe.

so a predicate for truth would be written T[x], with x a variable, and in set theory, it would say that the point x is true if and only T[x] ??

>>7785050
>so a predicate for truth would be written T[x], with x a variable, and in set theory, it would say that the point x is true if and only T[x] ??
but then truth relates to predicates and not to variables. it does not make sense to say ''let x be true''. this is what I do not follow

>>7785050
>so a predicate for truth would be written T[x], with x a variable, and in set theory, it would say that the point x is true if and only T[x] ??

Yea, that's what we mean by "truth predicate". Tarski's theorem says that such a predicate cannot be defined.
Because whenever you have the power of Peano's arithmetic, you can start defining autoreferential statements.
For example, define F = ¬T(F), and you can easily derive a contradiction, since F is true iff it is false.
That's just the old "this sentence is false" paradox formalized a little bit.

You obtain Gödel's theorem by just changing the word "true" by "provable", which IS definable. The trick is the same, define F = ¬Provable(F), and you get that F is neither provable nor unprovable.

>>7785078
>neither provable nor unprovable.
Messed up my vocabulary, I meant, neither provably true not provably false.
F is unprovable

>>7785082
ffs
F is not provable
¬F is not provable
Thus F is undecidable

>>7785078
>F = ¬T(F),
but since you have a predicate T[-] which takes a formula F, instead of a variable x, are you in second order logic ?

Gödel says that there's no formal system that can contain every single true theorem, thus every single formal system is incomplete.

Right?

I don't really remember how that's obtained from the recursion

>>7785342
oh ok I re-read the impossible statement

>>7785105
F = ¬ T[ GodelEncoding(F) ]

>>7785078
>For example, define F = ¬T(F)
Could you write out what you mean here? I've studied only a tiny bit of logic and in my head this reads
> F is equal to the negation of F being true (ie F is equal to F being false)
Where F means false I'm guessing.
How can we define something in this way?
Could you type out how you would read and interpret that phrase in your head?
I feel I'm reading it incorrectly.

>>7785014
Your response confused me a little. Can you elaborate what you mean by

>In other words you can test whether a statement is false

and

>Hence you can test if a statement is true but you cannot test if a statement is false.

Sounds like a contradiction. Having trouble wrapping my head what you meant.

Thanks

>>7785795
Ok. These are the important technical details to prove gödel's theorem.
- You can associate a unique integer [φ] to every logic formula φ (called the "gödel encoding" of φ). This was a new idea when Gödel did it, but nowadays it is an obvious thing : everything is numbers inside computers. Write out the formula in latex and the code of the pdf generated file is your number.
- You can define a predicate Provable(x) such that Provable( [φ] ) is true iff φ is provable.
- You can define auto-referential formulas. This is simiar to how you can write "Quine" programs in any programming language ( https://en.wikipedia.org/wiki/Quine_%28computing%29 ). You can define a formula φ such that inside the definition, it refers to [φ].

Thus, define the formula φ := ¬ Provable( [φ] ), and awesomeness ensues.

Tarski's theorem is the same, but instead of the "Provable" predicate, you assume there is a predicate "True" such that True( [φ] ) is true iff φ is true.
Then looking at the formula φ := ¬ True( [φ] ), you reach a contradiction.

>>7786070
How do you read
> φ := ¬ Provable( [φ] )

In english? Logical formula φ is equal to a non-provable godel encoding of φ?

So φ is true when φ is true but it's a contradiction because of the way φ is defined?

>>7786166
"define φ as the formula which expresses the non-provability of itself"

It is not a contradiction. It allows you to prove that either your logical system is inconsistent, either there is at least one formula (namely, φ) which cannot be proved, and whose negation cannot be proved.

For if you assume that φ is provable, then by definition you can prove ¬Provable( [φ] ), and you obtain a contradiction. If you assume ¬φ is provable, this implies that φ is not provable, and thus you can prove "¬Provable( [φ] )", which is, by definition, φ. Contradiction again

>>7786070
>Provable(x)
to be clear, this predicate lives in the theory of the arithmetic that you choose to consider ?

and your formula φ lives in what theory ? or does φ is a formula of the pure logic FOL ?