876: Structural Proof Theory/8

Tue Mar 2 07:27:07 EST 2021

 DETERMINISTIC QUANTITATIVE THEORY ASSOCIATED WITH PROOF ASSISTANTS

Let phi be a sentence in the first order predicate calculus with
equality. We will assume that we have already put phi into prenex
normal form.

We now define what we mean by THE TEST sequence for phi. This is the
infinite sequence S1,S2,S3,...  where each Si is a finite set of
sentences. From the THEORETICAL standpoint, I very much like that this
is a DETERMINISTIC PROCESS.

We will assume that phi has been put into prenex form via the standard
prenex normal form algorithm. Here is the construction of the TEST
sequence for phi. We assume a supply of constant symbols c1,c2,... not
mentioned in phi.

1. S1 consists of just phi.
2. S_i+1 results from S1,...,Si by
2a. For each sentence (therexists v)(psi) in S1 U ... U Si put
psi[v/c] in S_i+1. The c's must not appear in S1 U ... U Si and must
be distinct.
2b. For each sentence (forall v)(psi) in S1 U ... U Si put all
psi[v/t] in S_i+1, where t is a closed term with using only the
constants, relations, and functions in S1 U ... U S_i, and where the
total number of occurrences of constants, relations, and functions is
at most i+1.

The TEST sequence for phi is said to be BAD if and only if the
quantifier free formulas that appear are not jointly PROPOSITIONALLY
SATISFIABLE WITH THE QUANTIFIER FREE AXIOMS OF EQUALITY. It is said to
be n-bad if and only if the quantifier free formulas that appear in
the first n terms are not jointly propositionally satisfiable with the
quantifier free axioms of equality.

THEOREM. phi is valid if and only if the test sequence for not(phi) is
bad if and only if for some n, the test sequence for not(phi) is
n-bad.

*THIS IS MERELY A PARTICULARLY FRIENDLY NEAT SIMPLE SATISFYING FORM OF
WHAT IS COMMONLY KNOWN AS HENKINIZATION*

Notice that you immediately get a very clean completeness theorem
based on universal and existential instantiation. Also you can just
use conjunctive and disjunctive instantiation,

DEFINITION. The validity number for phi is the least n such that the
confirming sequence for not(phi) is n-bad.

CONJECTURE. It is interesting and fruitful and challenging to compute
exact or good estimates on validity numbers.

There is of course a gigantic supply of confirmed logical validities
out there generated by the proof assistants. Here we of course are not
going back to primitive notation but are using libraries of defined
constant, relations, and functions.

It is to be expected that these validity numbers are generally going
to get very large. But looking at actual proofs of validity, either
generated by proof assistants or by hand, one can use that information
to prove theorems about the validity numbers even if the relevant
sizes of the sets are incredibly huge. One has to identify the
portions of these enormous objects that are causing the badness.

It is clear that the powerful SAT solvers should be a vital tool in
these investigations.

QUESTION: What can we say about these validity numbers for theorems of
ZFC across mathematics? Let us say we have a theorem A of ZFC. We then
get validities of the form B implies A where B is a conjunction of
axioms from ZFC. Of course in general we are building off of a library
of defined constants, relations, and functions. What is the
relationship between our validity number for B implies A as we choose
different B's?

##########################################

My website is at https://u.osu.edu/friedman.8/ and my youtube site is at
https://www.youtube.com/channel/UCdRdeExwKiWndBl4YOxBTEQ
This is the 875th in a series of self contained numbered
postings to FOM covering a wide range of topics in f.o.m. The list of
previous numbered postings #1-799 can be found at
http://u.osu.edu/friedman.8/foundational-adventures/fom-email-list/

800: Beyond Perfectly Natural/6  4/3/18  8:37PM
801: Big Foundational Issues/1  4/4/18  12:15AM
802: Systematic f.o.m./1  4/4/18  1:06AM
803: Perfectly Natural/7  4/11/18  1:02AM
804: Beyond Perfectly Natural/8  4/12/18  11:23PM
805: Beyond Perfectly Natural/9  4/20/18  10:47PM
806: Beyond Perfectly Natural/10  4/22/18  9:06PM
807: Beyond Perfectly Natural/11  4/29/18  9:19PM
808: Big Foundational Issues/2  5/1/18  12:24AM
809: Goedel's Second Reworked/1  5/20/18  3:47PM
810: Goedel's Second Reworked/2  5/23/18  10:59AM
811: Big Foundational Issues/3  5/23/18  10:06PM
812: Goedel's Second Reworked/3  5/24/18  9:57AM
813: Beyond Perfectly Natural/12  05/29/18  6:22AM
814: Beyond Perfectly Natural/13  6/3/18  2:05PM
815: Beyond Perfectly Natural/14  6/5/18  9:41PM
816: Beyond Perfectly Natural/15  6/8/18  1:20AM
817: Beyond Perfectly Natural/16  Jun 13 01:08:40
818: Beyond Perfectly Natural/17  6/13/18  4:16PM
819: Sugared ZFC Formalization/1  6/13/18  6:42PM
820: Sugared ZFC Formalization/2  6/14/18  6:45PM
821: Beyond Perfectly Natural/18  6/17/18  1:11AM
822: Tangible Incompleteness/1  7/14/18  10:56PM
823: Tangible Incompleteness/2  7/17/18  10:54PM
824: Tangible Incompleteness/3  7/18/18  11:13PM
825: Tangible Incompleteness/4  7/20/18  12:37AM
826: Tangible Incompleteness/5  7/26/18  11:37PM
827: Tangible Incompleteness Restarted/1  9/23/19  11:19PM
828: Tangible Incompleteness Restarted/2  9/23/19  11:19PM
829: Tangible Incompleteness Restarted/3  9/23/19  11:20PM
830: Tangible Incompleteness Restarted/4  9/26/19  1:17 PM
831: Tangible Incompleteness Restarted/5  9/29/19  2:54AM
832: Tangible Incompleteness Restarted/6  10/2/19  1:15PM
833: Tangible Incompleteness Restarted/7  10/5/19  2:34PM
834: Tangible Incompleteness Restarted/8  10/10/19  5:02PM
835: Tangible Incompleteness Restarted/9  10/13/19  4:50AM
836: Tangible Incompleteness Restarted/10  10/14/19  12:34PM
837: Tangible Incompleteness Restarted/11 10/18/20  02:58AM
838: New Tangible Incompleteness/1 1/11/20 1:04PM
839: New Tangible Incompleteness/2 1/13/20 1:10 PM
840: New Tangible Incompleteness/3 1/14/20 4:50PM
841: New Tangible Incompleteness/4 1/15/20 1:58PM
842: Gromov's "most powerful language" and set theory  2/8/20  2:53AM
843: Brand New Tangible Incompleteness/1 3/22/20 10:50PM
844: Brand New Tangible Incompleteness/2 3/24/20  12:37AM
845: Brand New Tangible Incompleteness/3 3/28/20 7:25AM
846: Brand New Tangible Incompleteness/4 4/1/20 12:32 AM
847: Brand New Tangible Incompleteness/5 4/9/20 1 34AM
848. Set Equation Theory/1 4/15 11:45PM
849. Set Equation Theory/2 4/16/20 4:50PM
850: Set Equation Theory/3 4/26/20 12:06AM
851: Product Inequality Theory/1 4/29/20 12:08AM
852: Order Theoretic Maximality/1 4/30/20 7:17PM
853: Embedded Maximality (revisited)/1 5/3/20 10:19PM
854: Lower R Invariant Maximal Sets/1:  5/14/20 11:32PM
855: Lower Equivalent and Stable Maximal Sets/1  5/17/20 4:25PM
856: Finite Increasing reducers/1 6/18/20 4 17PM :
857: Finite Increasing reducers/2 6/16/20 6:30PM
858: Mathematical Representations of Ordinals/1 6/18/20 3:30AM
859. Incompleteness by Effectivization/1  6/19/20 1132PM :
860: Unary Regressive Growth/1  8/120  9:50PM
861: Simplified Axioms for Class Theory  9/16/20  9:17PM
862: Symmetric Semigroups  2/2/21  9:11 PM
863: Structural Mapping Theory/1  2/4/21  11:36PM
864: Structural Mapping Theory/2  2/7/21  1:07AM
865: Structural Mapping Theory/3  2/10/21  11:57PM
866: Structural Mapping Theory/4  2/13/21  12:47AM
867: Structural Mapping Theory/5  2/14/21  11:27PM
868: Structural Mapping Theory/6  2/15/21  9:45PM
869: Structural Proof Theory/1  2/24/21  12:10AM
870: Structural Proof Theory/2  2/28/21  1:18AM
871: Structural Proof Theory/3  2/28/21  9:27PM
872: Structural Proof Theory/4  2/28/21  10:38PM
873: Structural Proof Theory/5  3/1/21  12:58PM
874: Structural Proof Theory/6
875: Structural Proof Theory/7

Harvey Friedman