[FOM] Absolute undecidability

Sat Sep 12 07:10:00 EDT 2015

Referring to the response of Timothy Chow cited below, there actually is a another problem with the definition I suggested in my previous posting: It does not cover the cases I am interested in! (A technical error, sorry.) At any rate, I think it is better to consider the particular forms of "information" mentioned in the theorem if my PP.

Best, Arne.

Sendt fra en Samsung Mobil

-------- Opprinnelig melding --------
Fra: fom-request at cs.nyu.edu
Dato:12.09.2015 05:57 (GMT+01:00)
Til: fom at cs.nyu.edu
Emne: FOM Digest, Vol 153, Issue 42

Send FOM mailing list submissions to
        fom at cs.nyu.edu

To subscribe or unsubscribe via the World Wide Web, visit
        http://www.cs.nyu.edu/mailman/listinfo/fom
or, via email, send a message with subject or body 'help' to
        fom-request at cs.nyu.edu

You can reach the person managing the list at
        fom-owner at cs.nyu.edu

When replying, please edit your Subject line so it is more specific
than "Re: Contents of FOM digest..."

Today's Topics:

   1. Re: Absolute undecidability (Timothy Y. Chow)
   2. From EFQ to Research 3---further reply to Harvey Friedman
      (Tennant, Neil)
   3. Reply to Harvey Friedman's embedded letter from Avigad
      (Tennant, Neil)

----------------------------------------------------------------------

Message: 1
Date: Fri, 11 Sep 2015 18:37:25 -0400 (EDT)
From: "Timothy Y. Chow" <tchow at alum.mit.edu>
To: fom at cs.nyu.edu
Subject: Re: [FOM] Absolute undecidability
Message-ID: <alpine.LFD.2.11.1509111821370.26842 at laurent.mit.edu>
Content-Type: TEXT/PLAIN; charset=US-ASCII; format=flowed

Arne Hole wrote:

> We say that an infinite bit sequence {b_n} is a TAIL of the infinite bit
> sequence {a_n} if there a natural number k such that b_n=a_(n+k)  for
> all natural numbers n. Then we may say that a property P of infinite bit
> sequences definable in L(PA) is NONTRIVIAL (wrt to an infinite number of
> bits) iff it has the following properties:
>
> (i) If {a_n} has the property P , then all tails of {a_n} also have the
> property P
>
> (ii) The probability that an infinite p = 0.5 Bernoulli sequence has the
> property P, is less than 1.

This is precise, but I wonder how plausible it is that we cannot obtain
nontrivial knowledge in this sense.

There are a number of conjectures that hypothesize that some object that
we understand rather poorly behaves "randomly."  For example, it is
commonly conjectured that various irrational numbers are normal in every
base, and there are various heuristic techniques in number theory that
pretend that the prime numbers are random.  Although these conjectures are
plausible, they can sometimes go wrong.  There is a nice list on
MathOverflow of examples where a randomness heuristic fails:

http://mathoverflow.net/questions/11978/heuristically-false-conjectures

Regarding bit-expansions of numbers, it is perhaps not so well known to
non-number theorists that some things can be said about infinitely many
as-yet-uncomputed bits of (say) pi.  The irrationality measure of pi is
known to be less than 8.  This in particular implies that for all
sufficiently large n, the nth through the (8n)th bits of pi cannot all be
zero.  Of course, this is a very weak statement about the bits of pi, and
I don't think it can be turned into nontrivial information in your sense.
Still, examples of this sort make me a bit cautious about hypothesizing
that it is impossible to obtain nontrivial information in your sense.

Tim

------------------------------

Message: 2
Date: Sat, 12 Sep 2015 02:16:05 +0000
From: "Tennant, Neil" <tennant.9 at osu.edu>
To: "fom at cs.nyu.edu" <fom at cs.nyu.edu>
Cc: "Friedman, Harvey M." <hmflogic at gmail.com>
Subject: [FOM] From EFQ to Research 3---further reply to Harvey
        Friedman
Message-ID:
        <3188F1ACFDF24246BE3EB20656F10C5D51761262 at CIO-TNC-D2MBX04.osuad.osu.edu>

Content-Type: text/plain; charset="windows-1252"

There were some matters that I did not take up from Harvey's posting 'From EFQ to Research 3', and I need to deal with them here briefly.

"Neil refers to some technical notion of relevance from an earlier
posting. Since there are so many earlier postings, a short posting by
Neil restating this notion in simple words, without natural deduction
diagrams, would be helpful ..."

The posting that explained this notion of relevance in simple words was
'From EFQ to Research---reply to Harvey Friedman's questions 1-3',
http://www.cs.nyu.edu/pipermail/fom/2015-September/019084.html

That Harvey did not immediately recall this part of my posting in connection with the topic of relevance may be owing to the circumstance that I wrote of "extralogical-vocabulary-sharing", rather than relevance. So I shall repeat here, with minor additions, what I wrote about the topic. The minor additions are in uppercase, and are not meant to be understood as screaming.
___________________

[T]here is a very strong result about extralogical-vocabulary-sharing, for first-order Classical Core Logic. Let P be a Classical Core proof of the conclusion A from the set X of premises. (Note that A can be #.)
I SHALL NOW DEFINE A RELEVANCE CONDITION R(X,A). FOR EVERY SEQUENT X:A THAT IS PROVABLE IN CLASSICAL CORE LOGIC, WE HAVE R(X,A).
There are three cases to consider:
(1) X is empty (so A is a theorem).
(2) A is # (so X is inconsistent).
(3) X is non-empty, A is not #.
In Case (1), A will have both a positive and a negative occurrence of some primitive extralogical expression.
In Case (2), every sentence in X connects to every other sentence in X by means of a path on which any two neighboring sentences contain some same primitive extralogical expression with opposite parities.
In Case (3), X partitions into components that are internally connected in the way just described for Case (2) [where X was the sole component]. Every component X' of X contains some sentence B such that some primitive extralogical expression enjoys an occurrence in B and an occurrence in A of the same parity.

THIS RESULT WAS PROVED IN MY PAPER
?The Relevance of Premises to Conclusions of Core Proofs?, Review of Symbolic Logic, 8, no. XXX, 2015, pp. XXX-XXX, DOI: http://dx.doi.org/10.1017/S1755020315000040. The intrested reader can download a .pdf from my publications webpage . It's #6 under 'Articles'.

FAMILIARITY WITH THIS PAPER WILL BE PRESUMED IN ANY FURTHER CONTINUATION OF THIS DISCUSSION WITH HARVEY. I KNOW THAT THIS IMPOSES AN OBLIGATION TO READ CERTAIN PUBLISHED WORKS BY OTHERS IN REFEREED JOURNALS. I APOLOGIZE PROFUSELY TO ALL CONCERNED FOR IMPORTUNING THEM IN THIS WAY.

REMEMBER, THE COMMENTS IN UPPERCASE ARE NOT MEANT TO BE UNDERSTOOD AS SCREAMED.

_______________________

"I am still entirely skeptical on whether this work of Tennant offers
up anything for the rather advanced and involved prover world, for any
of the usual calculi."

And the reasoned basis for such skepticism is ... ? And after reading my book Autologic when?...

"I am starting to ask that community whether
issues such as restricting EFQ or cut play any practical or
theoretical role in the Proof Assistant work. And generally, if they
have found any intelligible features of actual proofs that distinguish
them from possible proofs."

I can predict right away that this inquiry will be fruitless. How many of the informants in that community have even the remotest grasp of the subtleties and details of Core Logic? Will they have been following this discussion on FOM in the necessary detail, so as to be aware of the extent to which Core Logic's credentials have remained unscathed, despite the best efforts on the part of lifelong users of the orthodox systems to pick holes in it, or to find something they want logic to do but which Core Logic supposedly cannot do? I predict that Harvey will come back to this list with what he thinks is authoritative confirmation of his position; and the 'expert' criticisms thereby allegedly conveyed of Core Logic from that "rather advanced and involved" world will once again fall to rebuttal if ever the hearsay evidence becomes first-person testimony on this list.

Neil Tennant

-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20150912/990779f4/attachment.html>

------------------------------

Message: 3
Date: Sat, 12 Sep 2015 02:49:10 +0000
From: "Tennant, Neil" <tennant.9 at osu.edu>
To: "fom at cs.nyu.edu" <fom at cs.nyu.edu>
Cc: "Friedman, Harvey M." <hmflogic at gmail.com>
Subject: [FOM] Reply to Harvey Friedman's embedded letter from Avigad
Message-ID:
        <3188F1ACFDF24246BE3EB20656F10C5D51761272 at CIO-TNC-D2MBX04.osuad.osu.edu>

Content-Type: text/plain; charset="iso-8859-1"

"Most automated methods rely on classical reductions and/or rules that
presuppose EFQ."

And some don't---for example, all the proof-finders discussed in my book Autologic.

"In the constructive theorem proving community, most
people are convinced by the usual stories about the computational
interpretation of falsity, so I don't know of anyone in that community
that is keen to give that up."

Most people convinced by the usual stories tend to be attracted away from them when they finally learn of better stories. The problem is simply that of finding open minds that can absorb a new perspective and think about it.

"Of course, in higher-order systems, you can define "false" by "forall
P, P" in which case EFQ is valid. In Coq and Lean, it is defined by an
inductive definition (i.e. the empty one). So, in a sense, these
systems don't rely on EFQ, falsity is simply defined in a way that
makes it true."

# is a Bad Thing without having to imply every P.

"In short, I don't know of anyone seriously interested in avoiding EFQ.
Is there any good motivation to do so?"

Yes, very good motivation: it ensures relevance, does not sacrifice transitivity of deduction, and respects intuitions. Unfortunately, however, the suggestion that we can and should explore the benefits of avoiding EFQ gets some people really worked up!

"As far as using cut: in interactive theorem proving, of course, we
prove libraries of theorems and use them in proofs. So cut is used all
the time."

Note the adjective "interactive". But more importantly: we don't have to described this by saying "cut is used". That holds only if one actually applies a rule of cut in constructing a proof. One could, instead, simply refrain from cuts, and gather together all the sections of cut-free proof. It's what good writers of textbooks in mathematics actually do! That *there is* a proof of the 'overall' result is guaranteed by the cut-admissibility result.

"In resolution theorem proving, one proceeds by negating the
conclusion and trying to prove a contradiction with the resolution
rule, essentially "from 'A or B'  and 'not A' conclude B". So that is
sort of like a "cut calculus"."

I beg to differ. That is merely Disjunctive Syllogism, which holds in Core Logic. It should also be borne in mind that resolution theorem-proving falls far short of exhausting all the already extant approaches to fully automated deduction. Resolution theorem-proving derives from the pioneering book by Alan Robinson, 'Logic: Form and Function: the mechanization of deductive reasoning' (which I refereed for Edinburgh University Press).  My own approach to theorem proving, however, does not involve the resolution method. Ironically, though, since I program my proof-finders in that other great Edinburgh product, Prolog---which itself runs on the resolution method---I'm operating in resolution's shadow, so to speak. But it's really important to stress that the actual method of proof-search does not have to be a resolution method. It can instead be a method that seeks to mimic the way an expert logician searches for a proof of a given sequent. And it's amazing how much this effort!
  benefits from judiciously formulated, completeness-conserving normal-form theorems, which provide very exigent constraints on proof-search, thereby affording great speed-up. Also, Prolog is beautifully adapted to the framing of inductive definitions (of things like sentences and proofs), which is the bread and butter of computational logic.

"As far as "guessing" lemmas or
generalizations in automated reasoning, there has been some work along
these lines, but I don't know of any striking successes."

This is fully to be expected. I have already mentioned the computational costs of determining interpolants, in an earlier posting.

Harvey, there is absolutely nothing here to worry the Core Logician---just as I predicted.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20150912/0cc29234/attachment.html>

------------------------------

_______________________________________________
FOM mailing list
FOM at cs.nyu.edu
http://www.cs.nyu.edu/mailman/listinfo/fom

End of FOM Digest, Vol 153, Issue 42
************************************
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20150912/5b92707a/attachment-0001.html>