Path: utzoo!utgpu!jarvis.csri.toronto.edu!mailrus!nrl-cmf!ames!ucsd!sdcsvax!ucsdhub!hp-sdd!hplabs!hpda!hpwala!cfisun!ima!spdcc!merk!alliant!linus!mbunix!bwk
From: bwk@mbunix.mitre.org (Barry W. Kort)
Newsgroups: comp.ai
Subject: Re: Fun with the semantics of paradox
Summary: You can't prove it by me.
Keywords: Types, Paradoxes
Message-ID: <44268@linus.UUCP>
Date: 2 Feb 89 04:11:48 GMT
References: <1883@buengc.BU.EDU> <2996@uhccux.uhcc.hawaii.edu> <905@ubu.warwick.UUCP> <479@aipna.ed.ac.uk> <1036@hudson.acc.virginia.edu> <3715@uklirb.UUCP> <48717@yale-celray.yale.UUCP> <3781@uklirb.UUCP>
Sender: news@linus.UUCP
Reply-To: bwk@mbunix.mitre.org (Barry Kort)
Organization: True Value Software, Axon Causeway, NJ
Lines: 14

In article <3781@uklirb.UUCP> kerber@uklirb.UUCP (Manfred Kerber) writes:

 > One gets S1 <==> NOT S1.  It is a real paradox.

The paradox goes away if you admit the possibility that S1
is unprovable (or undecidable).  Then we merely have
that S1 is unprovable if and only if NOT S1 is unprovable.

Therefore I have proven that S1 is unprovable.
(I have also proven that NOT S1 is unprovable.)

Any questions?

--Barry Kort