http://plato.stanford.edu/entries/dialetheism/
second time I've linked to that ITT
again, hth
0816: "Applied Math"
Moderators: Moderators General, Prelates, Magistrates
Re: 0816: "Applied Math"
Something similar to this is something that's always bothered me about Godel's Incompleteness Theorem: the theorem shows that certain sufficiently expressive consistent axiomatic systems must be able to formulate statements which are true but unprovable from within that system. This is proven by showing that any such sufficiently expressive axiomatic system can produce formulae (which state in effect that they are unprovable within said system) which we can show by 'basic logic' (i.e. proof by contradiction, reductio ad absurdum) must either be provable from the axioms but thus demonstrably (from 'basic logic' alone) false, and the system thus inconsistent; or unprovable from the axioms but thus demonstrably (again from 'basic logic' alone) true, and the system thus incomplete.
But surely, ANY axiomatic system incorporates 'basic logic' (i.e. includes, at least implicitly, the principle of noncontradiction amongst its axioms); so ANY axiomatic system would be able to prove a Godel proposition, which states that it is unprovable; thus you should get a contradiction if you assign ANY truthvalue to a Godel proposition. Saying it's "true but unprovable" is just as much nonsense as saying it's "provable yet false". If you assign any truthvalue to it you end up having to also assign the other truth value to it, so either you must be able to assign both truth values to it (and the principle of noncontradiction is false) or you must be able to assign neither truth value to it (and the principle of the excluded middle is false). I'd rather discard the excluded middle than noncontradiction; but either way, the principle of bivalence (which equals noncontradiction plus the excluded middle) is false, and that's the lesson I take away from Godel: on pain of contradiction, we must conclude that some statements just don't have truthvalues. None of this "unprovable yet true" nonsense.
But surely, ANY axiomatic system incorporates 'basic logic' (i.e. includes, at least implicitly, the principle of noncontradiction amongst its axioms); so ANY axiomatic system would be able to prove a Godel proposition, which states that it is unprovable; thus you should get a contradiction if you assign ANY truthvalue to a Godel proposition. Saying it's "true but unprovable" is just as much nonsense as saying it's "provable yet false". If you assign any truthvalue to it you end up having to also assign the other truth value to it, so either you must be able to assign both truth values to it (and the principle of noncontradiction is false) or you must be able to assign neither truth value to it (and the principle of the excluded middle is false). I'd rather discard the excluded middle than noncontradiction; but either way, the principle of bivalence (which equals noncontradiction plus the excluded middle) is false, and that's the lesson I take away from Godel: on pain of contradiction, we must conclude that some statements just don't have truthvalues. None of this "unprovable yet true" nonsense.
Forrest Cameranesi, Geek of All Trades
"I am Sam. Sam I am. I do not like trolls, flames, or spam."
The Codex Quaerendae (my philosophy)  The Chronicles of Quelouva (my fiction)
"I am Sam. Sam I am. I do not like trolls, flames, or spam."
The Codex Quaerendae (my philosophy)  The Chronicles of Quelouva (my fiction)
 Yakk
 Poster with most posts but no title.
 Posts: 11129
 Joined: Sat Jan 27, 2007 7:27 pm UTC
 Location: E pur si muove
Re: 0816: "Applied Math"
The godel trick works because logic systems are not allowed to explicitly talk about their axioms typically.
So what the godel trick does is creates a copy of its own axioms and logic system within the logic system itself, then makes statements in that model inside of the logic system.
The logic system "does not know" that it is modeling itself, because the logic system is not selfaware.
We, as the person doing the fakeout on the logic system, do know that we are modeling the logic system itself within the logic system.
And we, because we know about the logic system, can see that the statements we are making in the model of the logic system are equivalent to statements in the logic system itself.
As it happens, the statements we are making in the model is equivalent to "this statement cannot be proven within the logic system". That is what it means within the model. We use a clever trick to make it also mean that same thing within the logic system, at least from our outside perspective.
We then, outside the system, ask "is there a proof for this statement". Well, presume there is a proof for this statement  then we have a proof that "this statement cannot be proven" is true. We then have a contradiction  a real, honest to goodness contradiction. We end up with T=F deduced by our logic system.
So there cannot be a proof for the logic statement. Yet that is exactly what we crafted our statement to say  that there is no proof for the statement.
The cleverness of Godel is that all of this is done with extreme care, so the technical hurdles of "you aren't allowed to talk about your own axioms" are avoided.
Note that systems that are allowed to talk about their own axioms end up selfdestructing under the Godel attack, sort of like the "set that contains all sets except itself" selfreference problem.
The trick isn't that our "basic logic" isn't included in the logic system, it is that logic systems are not designed to be "selfaware".
We have a system S. We have a basic logic system that is aware of S called B. We have a model of S within S called S'. We craft statements in S about S' that are true, but not provable, under arguments in B. S does not have access to B because S is not aware of itself, while B is aware of it. If S is aware of itself, the statements S we craft about S' end up generating a contradiction directly, as it is capable of modeling itself S within S, so that doesn't help.
Godel is about what statements can be proven in specific given sufficiently formal systems, not what statements can be proven. You can always strengthen your system to make the particular statement provable. Godel still applies to that new stronger system, but the statement you cannot prove (yet is true) is simply a different statement.
So what the godel trick does is creates a copy of its own axioms and logic system within the logic system itself, then makes statements in that model inside of the logic system.
The logic system "does not know" that it is modeling itself, because the logic system is not selfaware.
We, as the person doing the fakeout on the logic system, do know that we are modeling the logic system itself within the logic system.
And we, because we know about the logic system, can see that the statements we are making in the model of the logic system are equivalent to statements in the logic system itself.
As it happens, the statements we are making in the model is equivalent to "this statement cannot be proven within the logic system". That is what it means within the model. We use a clever trick to make it also mean that same thing within the logic system, at least from our outside perspective.
We then, outside the system, ask "is there a proof for this statement". Well, presume there is a proof for this statement  then we have a proof that "this statement cannot be proven" is true. We then have a contradiction  a real, honest to goodness contradiction. We end up with T=F deduced by our logic system.
So there cannot be a proof for the logic statement. Yet that is exactly what we crafted our statement to say  that there is no proof for the statement.
The cleverness of Godel is that all of this is done with extreme care, so the technical hurdles of "you aren't allowed to talk about your own axioms" are avoided.
Note that systems that are allowed to talk about their own axioms end up selfdestructing under the Godel attack, sort of like the "set that contains all sets except itself" selfreference problem.
The trick isn't that our "basic logic" isn't included in the logic system, it is that logic systems are not designed to be "selfaware".
We have a system S. We have a basic logic system that is aware of S called B. We have a model of S within S called S'. We craft statements in S about S' that are true, but not provable, under arguments in B. S does not have access to B because S is not aware of itself, while B is aware of it. If S is aware of itself, the statements S we craft about S' end up generating a contradiction directly, as it is capable of modeling itself S within S, so that doesn't help.
Godel is about what statements can be proven in specific given sufficiently formal systems, not what statements can be proven. You can always strengthen your system to make the particular statement provable. Godel still applies to that new stronger system, but the statement you cannot prove (yet is true) is simply a different statement.
One of the painful things about our time is that those who feel certainty are stupid, and those with any imagination and understanding are filled with doubt and indecision  BR
Last edited by JHVH on Fri Oct 23, 4004 BCE 6:17 pm, edited 6 times in total.
Last edited by JHVH on Fri Oct 23, 4004 BCE 6:17 pm, edited 6 times in total.
Re: 0816: "Applied Math"
Pfhorrest: Interesting. That seems at first glance like it would invalidate most forms of formal proof, though. If something can be neither true nor false, then proving it's not false doesn't prove it's true. And vice versa. You get a similar problem in programming. In some languages, a boolean value can only ever be true or false, so !x is equivalent to x==false is equivalent to !(x==true). In others, x can be null, so code stops working the way it looks like it should.
It seems like there could be a way around that; do you have one in mind?
It seems like there could be a way around that; do you have one in mind?
 Yakk
 Poster with most posts but no title.
 Posts: 11129
 Joined: Sat Jan 27, 2007 7:27 pm UTC
 Location: E pur si muove
Re: 0816: "Applied Math"
HonoreDB: eliminating the law of excluded middle isn't that alien. Proof by contradiction is pretty nonconstructive, so if you care about constructive truths, you tend to throw it out anyhow.
You end up being able to prove that !!!P(x) is equivalent to !P(x), but you cannot show that !!P(x) is equivalent to P(x), where P(x) is some proposition.
See
https://secure.wikimedia.org/wikipedia/ ... tuitionism
for logic that doesn't allow the law of excluded middle, and
https://secure.wikimedia.org/wikipedia/ ... ematics%29
for types of mathematics that reduces what kinds of basic logical operations are allowed.
If you are seriously into analysis:
https://secure.wikimedia.org/wikipedia/ ... e_analysis
but that is hard reading.
You end up being able to prove that !!!P(x) is equivalent to !P(x), but you cannot show that !!P(x) is equivalent to P(x), where P(x) is some proposition.
See
https://secure.wikimedia.org/wikipedia/ ... tuitionism
for logic that doesn't allow the law of excluded middle, and
https://secure.wikimedia.org/wikipedia/ ... ematics%29
for types of mathematics that reduces what kinds of basic logical operations are allowed.
If you are seriously into analysis:
https://secure.wikimedia.org/wikipedia/ ... e_analysis
but that is hard reading.
One of the painful things about our time is that those who feel certainty are stupid, and those with any imagination and understanding are filled with doubt and indecision  BR
Last edited by JHVH on Fri Oct 23, 4004 BCE 6:17 pm, edited 6 times in total.
Last edited by JHVH on Fri Oct 23, 4004 BCE 6:17 pm, edited 6 times in total.

 Posts: 98
 Joined: Fri Feb 19, 2010 5:48 am UTC
Re: 0816: "Applied Math"
more than two truth values are possible
in fact, infinitely many are!
depends what logic you want
not all formal systems are complex enough to generate a Gödel sentence
hth.
in fact, infinitely many are!
depends what logic you want
not all formal systems are complex enough to generate a Gödel sentence
hth.
Re: 0816: "Applied Math"
Yakk wrote:We have a system S. We have a basic logic system that is aware of S called B. We have a model of S within S called S'. We craft statements in S about S' that are true, but not provable, under arguments in B. S does not have access to B because S is not aware of itself, while B is aware of it. If S is aware of itself, the statements S we craft about S' end up generating a contradiction directly, as it is capable of modeling itself S within S, so that doesn't help.
My point of contention, though, is: aren't the axioms of B — or rather the axiom of B, the principle of noncontradiction, "for all x, ~(x^~x)" — a subset of the axioms of S, and S', or any consistent axiomatic system? Isn't that the very definition of "consistent": noncontradictory? So if you can prove Godel sentence G (written in S, about S') with B, you should be able to prove it with S, and even with S', since B is a subset of S and S' and any other consistent axiomatic system you'd care to invent.
It occurs to me that even that technical question aside, the more traditional interpretation of Godel still seems to support my general conclusion: (given consistency of all systems under discussion) no matter how many layers deep of axiomatic systems you "zoom out", you always have some sentence to which you cannot assign a truthvalue... not without "zooming out" another layer, which creates a new sentence to which you cannot assign a truthvalue, ad infinitum. Saying "either the principle of the excluded middle is false or the principle of noncontradiction is false", as I am, is essentially saying the same thing as "the system is either incomplete or inconsistent", except about any manylayered ensemble of axiomatic systems, rather than about any particular single axiomatic system. (Or perhaps it's saying that about "basic logic", which if formalized as above, as simply the principle of noncontradiction itself, would directly entail the falsehood of the principle of the excluded middle, as that would then read "NC => (~NC v ~EM)", which simplifies to just "~EM").
HonoreDB wrote:Pfhorrest: Interesting. That seems at first glance like it would invalidate most forms of formal proof, though. If something can be neither true nor false, then proving it's not false doesn't prove it's true. And vice versa. You get a similar problem in programming. In some languages, a boolean value can only ever be true or false, so !x is equivalent to x==false is equivalent to !(x==true). In others, x can be null, so code stops working the way it looks like it should.
It seems like there could be a way around that; do you have one in mind?
The beginnings of one at least, yes. It seems like it would be sufficient to treat most instances of "false" in existing proofs as meaning "untrue" instead (where "untrue" is a disjunction of "false" and "neither true nor false"), in which case doublenegation still works well enough. If it's not not true that P, then it's true that P. Where it would get tricky would be if you said something like "it's untrue that it's untrue that P".
To think of it symbolically in normal bivalent logical terms (though I'm not sure this would be the best practical way to implement this), maybe render all statements in existing proofs as gerund (so "F(x)" reads as the incomplete sentence "x being F", rather than "x is F") and then wrap them in a truthfunction which restores them to proper sentences (so if P is a gerundified proposition "x being F", then T(P) is the proper proposition "x is F").
So lets say there is a classical proof using doublenegation, like this simple example:
Code: Select all
1. P > (~Q)
2. Q
.: 3. ~(~Q) (from 2 via double negation)
.: 4. ~P (from 1 and 3 via modus tollens)
Or in English, "P implies that Q is false, but Q is true, therefore Q is not false, therefore P is false".
Rerendered as suggested above, that would now read:
Code: Select all
1. T(P) > (~T(Q))
2. T(Q)
.: 3. ~(~(T(Q)) (from 2 via double negation)
.: 4. ~(T(P) (from 1 and 3 via modus tollens)
Or in English, "P being true implies that Q is untrue, but Q is true, therefore Q is not untrue, therefore P is untrue".
This leaves the results of such proofs a little more vague than there would be classically, as it's not been shown whether P is false or whether it is neither true nor false. But we have established its truthlessness the same either way, and except in fringe cases like Godel sentences and patent nonsense (e.g. "this sentence green moo", as I think someone offered earlier in this thread) truthlessness is usually falseness. But hey, maybe if middleinclusive logics were accepted there might be some research to do looking back through old proofs to see if the nontruths they had established were genuine falsehoods or simple neithertruenorfalsehoods.
Yakk wrote:HonoreDB: eliminating the law of excluded middle isn't that alien. Proof by contradiction is pretty nonconstructive, so if you care about constructive truths, you tend to throw it out anyhow.
Noncontradiction and the excluded middle are not necessarily the same thing. Noncontradiction says ∀x¬(x∧¬x), whereas the excluded middle says ∀x(x∨¬x). For classical, bivalent logics, those two statements are equivalent, but for nonclassical logics like we're discussing they may come apart. Thus, just because you throw out one doesn't mean you have to throw out the other.
Forrest Cameranesi, Geek of All Trades
"I am Sam. Sam I am. I do not like trolls, flames, or spam."
The Codex Quaerendae (my philosophy)  The Chronicles of Quelouva (my fiction)
"I am Sam. Sam I am. I do not like trolls, flames, or spam."
The Codex Quaerendae (my philosophy)  The Chronicles of Quelouva (my fiction)
Re: 0816: "Applied Math"
On a slightly separate note though, Is it possible to have a system that has a sufficiently consistent inconsistency such that the inconsistency doesn't affect the majority of "consistent" calculations, hence bypassing most issues regarding consistency?
I am NOT a snake.
Opinions discussed are not necessarily the opinions of the people discussing them.
Opinions discussed are not necessarily the opinions of the people discussing them.
Re: 0816: "Applied Math"
Kyrn wrote:On a slightly separate note though, Is it possible to have a system that has a sufficiently consistent inconsistency such that the inconsistency doesn't affect the majority of "consistent" calculations, hence bypassing most issues regarding consistency?
Paraconsistent logic. Unfortunately this renders the Principle of Explosion false leaving me unable to shack up with your mom.
Forrest Cameranesi, Geek of All Trades
"I am Sam. Sam I am. I do not like trolls, flames, or spam."
The Codex Quaerendae (my philosophy)  The Chronicles of Quelouva (my fiction)
"I am Sam. Sam I am. I do not like trolls, flames, or spam."
The Codex Quaerendae (my philosophy)  The Chronicles of Quelouva (my fiction)
Return to “Individual XKCD Comic Threads”
Who is online
Users browsing this forum: No registered users and 38 guests