Started reading this short book on model theory I came across. It's a field I keep hearing about bizarre meta-mathematical results from, which I'm hoping to understand a bit better. Also apparently model theory is the origin of non-standard analysis.

P2451
I normally think of non-standard analysis in the context of being a way of working with the reals in acl2. Since normally acl2 (and lisp generally) just has the rationals.
https://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/index-seo.php/COMMON-LISP____REAL?path=3703/6631/819
https://www.cs.uwyo.edu/~ruben/static/pdf/nsa.pdf

>Since ACL2 is a first-order logic with only limited support for quantification, it seems far too weak to reason about the reals. Consider, for example, the least upper bound axiom, which states that every bounded set of real numbers has a least upper bound. This simple fact can not be expressed in ACL2, since ACL2 does not have a first-class notion of infinite set. In this paper, we will present a brief overview of non-standard analysis, first presented by Robinson as a formalization of infinitesimal calculus [31]. The main contribution of this paper will be to show that non-standard analysis provides a suitable framework for reasoning about the irrationals in ACL2. Moreover, this formalization should also be applicable to other theorem provers with support for induction.

Interesting. Can ACL2 reason about functions? If so, then can't the idea of a set of real numbers be expressed as a function (not necessarily computable) from the real numbers to true/false? Or is the real issue here "limited support for quantification"? What are the limits of ACL2's handling of quantifiers?

>What are the limits of ACL2's handling of quantifiers?
Reading the text a bit further, I think it answered my question: proofs involving quantifiers often require the quantifiers to be instantiated, e.g. proving "there exists an x such that blah blah" by giving such an x. But ACL2 cannot come up with the appropriate term unless it occurs elsewhere in the problem.

Briefly
P2595
Since it just thinks there are rational numbers by default, the classic result is that the number satisfying (equal (expt x 2) 2) does not exist. This isn't that big a problem most of the time.
>What if we came up with a function #'realp that let us know whether a number was real
I think this ability is where standardp pretty much gets us, based on non-standard analysis.
P2628
:doc quantifiers
ACL2 supports first-order quantifiers [exists] and [forall] by way of the [defun-sk] event. However, proof support for quantification is quite limited. Therefore, you may prefer using recursion in place of defun-sk when possible (following common ACL2 practice).
[examples]

Incidentally, there's apply$ for working with lambda forms but I don't really use it.

This is the ultimate troll math.

>Sir, I've got a complaint that you've been using infinitely large integers.

Yes I am. I take these statements as axioms:
c>1, c>2, c>3, c>4, c>5, c>6, c>7, c>8, c>9, c>10, c>11, c>12, c>13, c>14, c>15, ...
I await a disproof at your convenience.

But please note that if you expect me to actually read your proof, you may only use finitely many axioms.

>Hmm, maybe I can do it with "c>2, c>5, c>7, and c>15." If I just...

Good luck! If you succeed, congratulations on your disproof of 16!

>[every obscenity known to man]

Gödel: Remember, kids, if it's consistent, it exists. In a far-off corner of Plato's realm called Cantor's paradise. I can show you how to get there, but not if you're the Antichrist.

P3083
Okay, I'll actually read it this weekend.

Basically the subject is about the question "what if all these math symbols were really talking about something else?"

P3084
*Start reading it this weekend. I'm not used to this discussion of models, languages and theories so I have to think a lot about what's being said. I'm having trouble anchoring it to something I think is normal, though it seems like a promising way to think.

>loss of generosity
?

Generosity is important, wouldn't want to lose that.

Seems to have shown up around 2009 according to
https://forum.wordreference.com/threads/without-loss-of-generosity.2577757/

>Theorem 1. The Compactness Theorem (Malcev)
>A set of sentences is satisfiable iff every finite subset is satisfiable.

>Proof. There are several proofs. We only point out here that it is an easy
>consequence of the following theorem which appears in all elementary logic texts:

>Proposition. The Completeness Theorem (Godel, Malcev)
>A set of sentences is consistent if and only if it is satisfiable.

Kind of disappointing, but I can understand why he didn't want to add a discussion of proofs as it would greatly increase the length of the book. Guess I'm going to have to consult a logic textbook too. Baez's list recommends Enderton.

From Enderton's logic book. This is what you get for working in ZFC.

Enderton eases into the topic by first proving a babby compactness theorem for propositional logic only. Before reading his proof, shall we see if we can prove it ourselves?

The setting is pic related. For each natural number, we have a variable representing a sentence. We also have the usual logical connectives of propositional logic. We can use these to combine the sentence variables into formulas, which are called well-formed if they are written with correct syntax. Given a function that assigns true or false to each sentence variables, we can work out the truth value of any well-formed formula.

A set of well-formed formulas is called satisfiable if there is some way of assigning truth values to the sentence variables to make all the formulas work out true. For example, {(~ A2), (A1 \/ A2)} is satisfiable because both formulas are true when A1 is true and A2 is false. However, {(A1 -> A2), (A1 /\ (~ A2))} is not satisfiable as there is no truth assignment that makes both formulas true, as can be seen by the following truth table:

A1 A2 (~ A2) (A1 -> A2) (A1 /\ (~ A2))
T T F T F
T F T F T
F T F T F
F F T T F

The theorem we want to prove says that an infinite set of well-formed formulas is satisfiable if every finite subset is satisfiable.

P3872
Here's what I came up with.

[spoiler: Let S be a set of well-formed formulas such that every finite subset of S is satisfiable.

We first construct a series of partial truth assignments v₀, v₁, v₂, v₃, ..., where each vₙ assigns truth values to the first n variables, and each vₙ₊₁ is an extension of its predecessor vₙ (meaning vₙ₊₁(Aₖ) = vₙ(Aₖ) for k ≤ n). We will show that for each n, every finite subset of S is satisfied by a truth assignment that agrees with vₙ. For brevity we will write "S is satisfied by a truth assignment that agrees with vₙ" as "S is satisfiable by vₙ."

We proceed by induction. The base case n=0 is equivalent to the original hypothesis. Assume that every finite subset of S is satisfiable by vₙ. We must show that there is a vₙ₊₁ that extends vₙ with a value for vₙ₊₁(Aₙ₊₁), such that every finite subset of S is satisfiable by vₙ₊₁. There are two candidates for vₙ₊₁; let t be one that makes t(Aₙ₊₁) true, and let u be the one that makes u(Aₙ₊₁) false. Assume the opposite of what we want to prove, namely that there is a finite subset Q of S not satisfiable by t, and there is a finite subset R of S not satisfiable by u. Then Q ∪ R is a finite subset of S satisfiable neither by t nor u. But if Q ∪ R is neither satisfiable by t nor u, it is not satisfiable by vₙ, contradicting our inductive hypothesis.

Since all of the v₀, v₁, v₂, v₃, ... are consistent with each other, we can combine them to obtain a truth assignment v which assigns truth values to all variables. We now show that v satisfies all formulas in S. Let F be a formula in S, and let n be the highest index of the variables that occur in F. Then {F} is a finite subset of S, and it is satisfiable by vₙ. Since v agrees with vₙ for the truth assignments of all variables that occur in F, v satisfies F.]

P3591
Part of the proof of the completeness theorem. Am I wrong in thinking this is basically equivalent to adding Hilbert's ε operator?