0816: "Applied Math"

This forum is for the individual discussion thread that goes with each new comic.

Moderators: Moderators General, Prelates, Magistrates

Turing Machine
Posts: 98
Joined: Fri Feb 19, 2010 5:48 am UTC

Re: 0816: "Applied Math"

Postby Turing Machine » Fri Nov 12, 2010 6:38 am UTC

http://plato.stanford.edu/entries/dialetheism/

second time I've linked to that ITT

again, hth

User avatar
Pfhorrest
Posts: 5474
Joined: Fri Oct 30, 2009 6:11 am UTC
Contact:

Re: 0816: "Applied Math"

Postby Pfhorrest » Fri Nov 12, 2010 8:04 pm UTC

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 non-contradiction 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 truth-value 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 truth-value 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 non-contradiction 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 non-contradiction; but either way, the principle of bivalence (which equals non-contradiction 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 truth-values. 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)

User avatar
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"

Postby Yakk » Fri Nov 12, 2010 8:18 pm UTC

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 self-aware.

We, as the person doing the fake-out 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 self-destructing under the Godel attack, sort of like the "set that contains all sets except itself" self-reference 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 "self-aware".

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.

HonoreDB
Posts: 161
Joined: Tue Feb 06, 2007 4:32 pm UTC
Contact:

Re: 0816: "Applied Math"

Postby HonoreDB » Fri Nov 12, 2010 8:18 pm UTC

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?

User avatar
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"

Postby Yakk » Fri Nov 12, 2010 8:28 pm UTC

HonoreDB: eliminating the law of excluded middle isn't that alien. Proof by contradiction is pretty non-constructive, 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.
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.

Turing Machine
Posts: 98
Joined: Fri Feb 19, 2010 5:48 am UTC

Re: 0816: "Applied Math"

Postby Turing Machine » Fri Nov 12, 2010 11:44 pm UTC

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.

User avatar
Pfhorrest
Posts: 5474
Joined: Fri Oct 30, 2009 6:11 am UTC
Contact:

Re: 0816: "Applied Math"

Postby Pfhorrest » Sat Nov 13, 2010 4:40 am UTC

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 non-contradiction, "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": non-contradictory? 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 truth-value... not without "zooming out" another layer, which creates a new sentence to which you cannot assign a truth-value, ad infinitum. Saying "either the principle of the excluded middle is false or the principle of non-contradiction is false", as I am, is essentially saying the same thing as "the system is either incomplete or inconsistent", except about any many-layered 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 non-contradiction 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 double-negation 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 truth-function 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 double-negation, 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".

Re-rendered 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 middle-inclusive logics were accepted there might be some research to do looking back through old proofs to see if the non-truths they had established were genuine falsehoods or simple neither-true-nor-false-hoods.

Yakk wrote:HonoreDB: eliminating the law of excluded middle isn't that alien. Proof by contradiction is pretty non-constructive, so if you care about constructive truths, you tend to throw it out anyhow.

Non-contradiction and the excluded middle are not necessarily the same thing. Non-contradiction 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)

Kyrn
Posts: 937
Joined: Sat Sep 05, 2009 3:55 pm UTC
Location: The Internet

Re: 0816: "Applied Math"

Postby Kyrn » Sat Nov 13, 2010 1:57 pm UTC

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.

User avatar
Pfhorrest
Posts: 5474
Joined: Fri Oct 30, 2009 6:11 am UTC
Contact:

Re: 0816: "Applied Math"

Postby Pfhorrest » Sat Nov 13, 2010 9:27 pm UTC

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)


Return to “Individual XKCD Comic Threads”

Who is online

Users browsing this forum: No registered users and 38 guests