877: Structural Proof Theory/9
Harvey Friedman
hmflogic at gmail.com
Wed Mar 3 00:19:46 EST 2021
DETERMINISTIC QUANTITATIVE THEORY ASSOCIATED WITH PROOF ASSISTANTS
IMPROVED PRESENTATION
UNIVERSALITY OF SAT SOLVING BUSINESS?
Start with a sentence A in first order predicate calculus WITHOUT
equality. It is simpler to normally conjunct A with the axioms of
equality in the language of A, but regard that as OPTIONAL.
STEP 1. We start by forming the language L*(A) expanding the language
L(A) of A. L*(A) is an expansion of L by constant symbols only, called
Henkin Constants. Every sentence phi of L*(A) comes with a unique
constant symbol c(phi) associated with it. This uniquely defines the
language L*(A) and the association of constants c(phi) to all
sentences in L*(A), which is unique up to a name change for the
constants. HENKIN constants.
STEP 2. Put A in prenex form with the standard prenex normal form
algorithm, and then put the quantifier free part into CONJUNCTIVE
normal form. Call this A'.
STEP 3. We now form the set A* of all sentences in L*(A) generated in
the following way starting with A'. Each phi in A* of the form (there
exists v)(psi) generates psi[v/c(phi)]. Each phi in A* of the form
(for all v)(psi) generates all of the psi[v/t] where t is a closed
term in L*. THUS WE CAN SAY THAT A* is the set GENERATED BY
EXISTENTIAL AND UNIVERSAL INSTANTIATION starting with A'.
STEP 4. We now look at ONLY THE QUANTIFIER FREE sentences in A*,
recall that they are all in conjunctive normal form, and apply
conjunctive instantiation. This gets rid of all of the conjunction
signs, resulting in the set A** of sentences. Each of the sentences in
A** is a DISJUNCTION OF LITERALS. I.e., a DISJUNCTION OF ATOMIC
SENTENCES AND NEGATED ATOMIC SENTENCES from L*(A).
STEP 5. A REALIZATION of A** consists of a choice of one literal from
each element of A** where there is no conflict. I.e., where no atomic
sentence appears along with its negation.
THEOREM 1. A is satisfiable if and only if A** has a realization. A is
refutable if and only if A** has no realization. A is provable if and
only if (notA)** has no realization.
THEOREM 2. A** has a realization if and only if every finite subset of
A** has a realization. A** has no realization if and only if some
finite subset of A** has no realization.
THEOREM 3. A is valid if and only if some finite subset of (notA)**
has no realization.
WE NOW CAN ASSOCIATE INTEGERS TO VALID A.
1. The least cardinality of a finite subset of (notA)** with no realization.
2. The least cardinality of the union of a finite subset of (notA)**
with no realization.
3. The least complexity of a finite subset of (notA)** with no realization.
In 3, we can use complexity of a finite set of finite sets of literals
as the total number of occurrences of constant, relation, and function
symbols.
There is yet another interesting integer associated to valid A. IN
SOME VIEWPOINTS THIS NOTION I AM GOING TO MENTION NOW, could be even
more interesting THEORETICALLY.
In STEP 3, the formation of A*, we can break this down into infinitely
many stages. Start with A. Then do existential and universal
instantiation for L(A) only, yielding A*[1]. Then do existential and
universal instantiation for L(A*[1]) only, yielding A*[2]. And so
forth. Then define A**[n] to be only the quantifier free sentences in
A*[n].
THEOREM 4. A is satisfiable if and only if every A**[n] has a
realization. A is valid if and only if some (notA)**[n] has no
realization.
4. The least n such that (notA)**[n] has no realization.
So 4 is sensitive only to some sort of overall depth of the validity,
where we don't take into account the complexity of the instantiations
involved. There are other variant ideas on the quantities to be picked
out, with various combinations of considerations.
A POSSIBLE LESSON. The whole SAT SOLVING BUSINESS can be viewed as
intimately connected with the entire PURE MATHEMATICS CORPUS - at
least theoretically.
##########################################
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 877th 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 3/1/21 6:52PM
875: Structural Proof Theory/7 3/2/21 4:07AM
876: Structural Proof Theory/8 3/2/21 7:27AM
Harvey Friedman
More information about the FOM
mailing list