From d18e7f9b8417b65affa532b3339b5d868fe320e2 Mon Sep 17 00:00:00 2001 From: Guillaume Babin Date: Tue, 6 Jun 2017 17:35:10 +0200 Subject: [PATCH] Fix typos --- posts/tlaplus_part2.html | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/posts/tlaplus_part2.html b/posts/tlaplus_part2.html index 1b6ec05..a846e2c 100644 --- a/posts/tlaplus_part2.html +++ b/posts/tlaplus_part2.html @@ -361,7 +361,7 @@

First Order Logic and Other OrdersNow, notice that the model for a FOL formula, say $x > 2$, is always a set of values from the universe (in this case, all numbers greater than 2). So the model of a FOL formula is always a second-order object. But if the meaning of a formula is a set, a second-order object, then how can we write a general axiom such as $\vdash A \lor \neg A$ where $A$ stands not for a specific formula but for any formula? We can’t write $\A A . A \lor \neg A$ because we can’t quantify over formulas (which, as we’ve just seen, stand for sets, or second-order values) nor treat them as free variables for the same reason. The answer is that we don’t. We say that such an axiom is an axiom schema that refers to an infinite number of axioms in the logic, one for each possible formula $A$. The language used to write the schema is therefore not the logic itself, but the metalogic, or metalanguage of our logic.

-

While this is fine from a theory standpoint, this is not satisfactory for a mechanical proof software. When proving a theorem, we often need to prove may intermediate steps, and we would like to be able to state and prove general lemmas which we could reuse in many proofs, and such general second-order lemmas can be very useful.

+

While this is fine from a theory standpoint, this is not satisfactory for a mechanical proof software. When proving a theorem, we often need to prove many intermediate steps, and we would like to be able to state and prove general lemmas which we could reuse in many proofs, and such general second-order lemmas can be very useful.

One solution is, therefore, to adopt a higher-order logic. HOL serves as the basis for the theorem provers Isabelle/HOL and HOL Light, and more arcane type theories, like the constructive theories used in Coq or Agda, are also higher-order. But keeping the logic first-order has some advantages in terms of simplicity, model checking algorithms, general theorems (if we know that a formula is first-order, it’s easier to state theorems about a formula’s meaning based on its syntactic structure) — the last one is more relevant for TLA, the temporal logic part of TLA+, which we’ll cover in the next installments. But it turns out that we can have our cake and eat it, too. We can keep all formulas first-order, but allow writing second-order propositions in the form $A \vdash B$, which are not in themselves formulas (and so they don’t have a model). We basically provide access to the metalanguage. This is the solution adopted by TLA+, which we’ll see later in the section about proofs.

@@ -905,7 +905,7 @@

Sequences and Tuples

-

We can apply such functions with the expression $foo[3, \str{hi}]$, which is just syntactic sugar for $f[\seq{3, \str{hi}}]$.

+

We can apply such functions with the expression $foo[3, \str{hi}]$, which is just syntactic sugar for $foo[\seq{3, \str{hi}}]$.

Records

@@ -1041,7 +1041,7 @@

Putting it All Together

We can later use this definition when we define algorithms over linked list to show that the type of the list is preserved. This turns the familiar notion of type into just another, relatively simple property we can specify and verify. For example, $x \in Node$ is just another proposition, like $a + b = 0$.

-

Now, let’s define a view that presents a linked list as a sequence. For simplicity, let’s assume we only allow finite lists. Remember, a finite sequence is just a function of some 1..n:

+

Now, let’s define a view that presents a linked list as a sequence. For simplicity, let’s assume we only allow finite lists. Remember, a finite sequence is just a function of some $1..n$: