Insights into Well-Structured Mathematical Logic and Formal Linguistics

A Twenty-Minute Glimpse of Well-Structured Mathematical Logic by Damon Scott Francis Marion University Presented at the 2016 Annual North American Meeting of the Association for Symbolic Logic at 6:00 p.m. on Wednesday, May 25 in Room 163 Austin Hall

A Twenty Minute Glimpse of Well-Structured Mathematical Logic General Principle: To get to the next mountain ridge, you must cross a deep valley. The Ridge You re On When formalized in Traditional Formal Logic (called Frege-Hilbert Syntax), mathematics is machine-parsable, but it is relentlessly, hopelessly, user-hostile and unworkable. The Next Ridge Over When formalized in Well-Structured Mathematical Logic, mathematics is machine-parsable, but it is also user-friendly, pliant, and easy.

A Twenty Minute Glimpse of Well-Structured Mathematical Logic The Valley in Between: The New Formal Linguistics is the way to the next ridge. Syntax can be phrased in three different ways: Nested: Syntax nested inside other syntax, already very familiar. Flowing: Syntax flowing after other syntax, such as Matrix Multiplication. Random-Accessed: Syntax jumbled together, such as Matrix Addition. All three methods of phrase structure ramify with themselves and with one another and yield diversified ramification. In general: Flowing and Random-Accessed structures are user-friendly, and nested structures are user-hostile. The Central Result of the New Formal Linguistics informs one exactly where one can place flowing and random-accessed phrase structures into a newly composed formal language and where one cannot place such structures. By making the greatest possible use of the flowing and random-accessed phrase structures, one may maximize user-friendliness into a newly composed formal language.

A Twenty Minute Glimpse of Well-Structured Mathematical Logic Let s Rephrase First-Order Logic! It will only take a few minutes if we just rephrase the language and not logical deduction and proof. So as to ensure that the phrase structure is clear, all notation of phrase structure is written out. Nested structures are indicated with parentheses or bracesets, ( ) or { } . Flowing structures are indicated with a comma, , . Random-accessed structures are not explicitly used in the new formalization. One may suppress notation of phrase structure on both the Ridge You re On and the Next Ridge Over when it is algorithmic to put the phrase structure back in. Still the phrase structure is every bit as much real and there even when it is implicit (that is, not written out).

A Twenty Minute Glimpse of Well-Structured Mathematical Logic We rephrase absolute truth and falsehood The Ridge You re On Not much going on here. 0 1 The Next Ridge Over Sans-serif dialect; semicolons will make one point of phrase structure work out later: 0;1; Semantics: Absolute (or boolean) falsehood Absolute (or boolean) truth

A Twenty Minute Glimpse of Well-Structured Mathematical Logic We rephrase negation The Ridge You re On Negation with full phrase structure displayed. ~ (P ) The Next Ridge Over Negation with full phrase structure displayed, sans-serif dialect n, P Now eliminate the last argument and arrive at this hungry function: n, Semantics: not

A Twenty Minute Glimpse of Well-Structured Mathematical Logic We rephrase the binary boolean operators The Ridge You re On Or and And with full phrase structure displayed: (P ) (Q) (P ) (Q) The Next Ridge Over Given and Required with full phrase structure displayed, sans-serif dialect: G {P }, Q R {P }, Q Now eliminate the last argument as before: G {P },R {P }, Semantics (which ramify by scale of expression): Small scale: if P, then P Middle scale: Assume P. We show P .* Large scale: Axiom: P. * or, We have shown P. The tense of the verb depends on the aspect of the clause, which you cannot even glimpse at in these twenty minutes. Theorem: P

A Twenty Minute Glimpse of Well-Structured Mathematical Logic We rephrase the quantifiers The Ridge You re On For-all and for-some with full formal phrase structure displayed: x . [Q ] x . [Q ] The Next Ridge Over For-all and for-some with full phrase structure displayed, sans-serif dialect: A {x }, Q E {x }, Q Now eliminate the last argument as before: A {x },E {x }, Semantics (which ramify by scale of expression): Small scale: for all x , for some x , Middle scale: Let x. Make x. Large scale: Let by definition x. Make by definition x.

A Twenty Minute Glimpse of Well-Structured Mathematical Logic We rephrase and reconceive of the such-that operator. The Ridge You re On Such-that is mere filler for the there-exists construction: x Q The Next Ridge Over Such-that is a first-class operator. It works in conjunction with the quantifiers to produce qualified quantifers. Here are two examples: A { }, st { > 0}, E { }, st { > 0}, Succeeding statments (main clauses) have already been eliminated.

A Twenty Minute Glimpse of Well-Structured Mathematical Logic We don t rephrase the substitution operators. Sorry! Lack of time does not allow this to be shown in your twenty-minute glimpse.

A Twenty Minute Glimpse of Well-Structured Mathematical Logic A Specimen: The Mean Value Theorem Informal Presentation (Not yet mathematical logic at all) THEOREM: Let a and b be real numbers with a < b. Let f ([a, b] ). Assume f is differentiable throughout (a, b), and assume that fis continuous ataand atb. Then there exists a real number c in (a, b) so that f (c) = (f (b) f (a)) / (b a).

A Twenty Minute Glimpse of Well-Structured Mathematical Logic Traditional (Frege-Hilbert) Formalization The Ridge You re On THEOREM: a . [ b . [(a < b) ( f ([a, b] ). [ ( ( x (a, b) . [f is differentiable at x] ) ( (f is continuous at a) (f is continuous at b) ) ) c (a, b). [ f (c) = (f (b) f (a)) / (b a)] ) ] ) ] ] If this is the product we re selling, there will be precious little demand for mathematical logic or for mathematical logicians.

A Twenty Minute Glimpse of Well-Structured Mathematical Logic Let s Start Over Informal Presentation THEOREM: Let a and b be real numbers with a < b. Let f ([a, b] ). Assume f is differentiable throughout (a, b), and assume that fis continuous ataand atb. Then there exists a real number c in (a, b) so that f (c) = (f (b) f (a)) / (b a).

A Twenty Minute Glimpse of Well-Structured Mathematical Logic We formalize at small scale Transitioning THEOREM: Let a, b a < b. Let f ([a, b] ). Assume f is differentiable throughout (a, b), and assume that fis continuous ataand atb. Then there exists a real number c in (a, b) so that f (c) = (f (b) f (a)) / (b a).

A Twenty Minute Glimpse of Well-Structured Mathematical Logic We formalize at small scale Transitioning THEOREM: Let a, b a < b. Let f ([a, b] ). Assume x (a, b), f is differentiable at x. Assume that f is continuous at a. Assume that f is continuous at b. Then c (a, b), f (c) = (f (b) f (a)) / (b a).

A Twenty Minute Glimpse of Well-Structured Mathematical Logic We have formalized at small scale At small scale, life on the two ridges is much the same. THEOREM: Let a, b a < b. Let f ([a, b] ). Assume x (a, b), f is differentiable at x. Assume that f is continuous at a. Assume that f is continuous at b. Then c (a, b), f (c) = (f (b) f (a)) / (b a).

A Twenty Minute Glimpse of Well-Structured Mathematical Logic We formalize at middle scale Start here THEOREM: Let a, b a < b. Let f ([a, b] ). Assume x (a, b), f is differentiable at x. Assume that f is continuous at a. Assume that f is continuous at b. Then c (a, b), f (c) = (f (b) f (a)) / (b a).

A Twenty Minute Glimpse of Well-Structured Mathematical Logic We formalize at middle scale Transitioning THEOREM: A { a, b }, st {a < b}, Let f ([a, b] ). Assume x (a, b), f is differentiable at x. Assume that f is continuous at a Assume that f is continuous at b. Then c (a, b), f (c) = (f (b) f (a)) / (b a).

A Twenty Minute Glimpse of Well-Structured Mathematical Logic We formalize at middle scale Transitioning THEOREM: A { a, b }, st {a < b}, A {f ([a, b] ) }, Assume x (a, b), f is differentiable at x. Assume that f is continuous at a. Assume that f is continuous at b. Then c (a, b), f (c) = (f (b) f (a)) / (b a).

A Twenty Minute Glimpse of Well-Structured Mathematical Logic We formalize at middle scale Transitioning THEOREM: A { a, b }, st {a < b}, A {f ([a, b] ) }, G { A {x (a, b)}, f is differentiable at x}, Assume that f is continuous at a. Assume that f is continuous at b. Then c (a, b), f (c) = (f (b) f (a)) / (b a).

A Twenty Minute Glimpse of Well-Structured Mathematical Logic We formalize at middle scale Transitioning THEOREM: A { a, b }, st {a < b}, A {f ([a, b] ) }, G { A {x (a, b)}, f is differentiable at x}, G { f is continuous at a}, G { f is continuous at b}, Then c (a, b), f (c) = (f (b) f (a)) / (b a).

A Twenty Minute Glimpse of Well-Structured Mathematical Logic We formalize at middle scale Transitioning THEOREM: A { a, b }, st {a < b}, A {f ([a, b] ) }, G { A {x (a, b)}, f is differentiable at x}, G { f is continuous at a}, G { f is continuous at b}, R {E {c (a, b) }, f (c) = (f (b) f (a)) / (b a) }, 1;

A Twenty Minute Glimpse of Well-Structured Mathematical Logic We have formalized at middle scale Look at that! THEOREM: A { a, b }, st {a < b}, A {f ([a, b] ) }, G { A {x (a, b)}, f is differentiable at x}, G { f is continuous at a}, G { f is continuous at b}, R {E {c (a, b) }, f (c) = (f (b) f (a)) / (b a) }, 1;

A Twenty Minute Glimpse of Well-Structured Mathematical Logic We even formalize at large scale Here we go! THEOREM: A { a, b }, st {a < b}, A {f ([a, b] ) }, G { A {x (a, b)}, f is differentiable at x}, G { f is continuous at a}, G { f is continuous at b}, R {E {c (a, b) }, f (c) = (f (b) f (a)) / (b a) }, 1;

A Twenty Minute Glimpse of Well-Structured Mathematical Logic We even formalize at large scale Transitioning R { A { a, b }, st {a < b}, A {f ([a, b] ) }, G { A {x (a, b)}, f is differentiable at x}, G { f is continuous at a}, G { f is continuous at b}, R {E {c (a, b) }, f (c) = (f (b) f (a)) / (b a) }, 1; },

A Twenty Minute Glimpse of Well-Structured Mathematical Logic We have formalized everything The Next Ridge Over R { A { a, b }, st {a < b}, A {f ([a, b] ) }, G { A {x (a, b)}, f is differentiable at x}, G { f is continuous at a}, G { f is continuous at b}, R {E {c (a, b) }, f (c) = (f (b) f (a)) / (b a) }, 1; },

A Twenty Minute Glimpse of Well-Structured Mathematical Logic One Touch of Context-Oriented Simplication Still on the Next Ridge Over R { M{The Mean Value Theorem}, A { a, b }, st {a < b}, A {f ([a, b] ) }, G { A {x (a, b)}, f is differentiable at x}, G { f is continuous at a}, G { f is continuous at b}, E {c (a, b) }, R { f (c) = (f (b) f (a)) / (b a) }, 1; },

A Twenty Minute Glimpse of Well-Structured Mathematical Logic