I wonder if computability and epistemology are ultimately not one and the same thing? — alcontali

You mistake the claim that all stipulated axioms and formal systems are useful or arbitrary or relevant in every sense for the much weaker claim that some stipulated axioms and formal systems are useful or arbitrary or relevant in some sense. — fdrake

Well, no. I do not even care if a formal system is useful or meaningful. — alcontali

I think you found your own answer, then.

For example, in what way is the SKI combinator calculus useful or meaningful? It is obviously neither. It is merely "interesting". — alcontali

You mistake the claim that all stipulated axioms and formal systems are useful or arbitrary or relevant in every sense for the much weaker claim that some stipulated axioms and formal systems are useful or arbitrary or relevant in some sense.

I am endorsing the second claim. I believe the second claim entails:

(1) There are justifications for choosing between different stipulated formal systems.
(2) These reasons are not part of any stipulated list of compared formal systems.
(3) and are thereby not algorithmically choose-able.
(4) These justifications are not arbitrary.

Hence, this real-world phenonemon falls outside the realm of what mathematics is supposed to study. — alcontali

In a very trivial sense, yes; the world is not constituted by mathematical symbols or formal systems. In a not so trivial sense, no; some mathematical symbols and formal systems may be used to describe the world or be useful for other purposes.

Hence, this real-world phenonemon falls outside the realm of what mathematics is supposed to study. — alcontali

Read: most of what epistemology studies falls outside the realm of what mathematics (and specifically computability theory) is supposed to study..

You're talking about what follows if you accept the axioms as true. Not about what justifies stipulating them in the first place. There are good axiomatisations and bad axiomatisations given purposes. If you want to stipulate a system which contains usual arithmetic, 1+1=2 better be a theorem...

"Every triangle has angles which sum to two right angles" accept or reject and on what basis? The latter basis is a sense of justification deeper than your portrayal of acceptance/rejection of axioms as arbitrary.

Sentence X can be utterly useless, and probably also meaningless, but it is nevertheless a justified (true) belief, with the term "true" referring to the fact that it is logically true in the model(s) for the theory embodying axiom A. — alcontali

A person living on a sphere arbitrarily stipulates that all triangles on the surface of their sphere sum to two right angles. Since he is clever, he concludes the parallel postulate using the rest of Euclidean geometry. On this basis, you say"Of course his stipulation is justified, the choice between axiom systems is entirely arbitrary, and look, he derived the parallel postulate from it". But he lives on a sphere, so the axiom turns out to be false.

We live in a more complicated world, so we do not have easy ways to tell how relevant our stipulations are for our purposes except by investigating their consequences; be they as theorems of formal systems, as predictions, as enabling insightful description... The axioms of formal systems are not immune to these considerations, and are thus not arbitrarily chosen or chosen algorithmically.

Why would a computer choose the Turing machine formalism over the arbitrary decision procedure formalism to talk about computation? It couldn't, without having some criterion.

Is that criterion arbitrary? No, it depends on what we're studying. Are we like Euclid, living on a sphere?

It will obviously be true within the model that satisfies your axiomatization. — alcontali

Unless I interpret the statement as false and study the consequences. :chin:

But yes, there is a component of choice in setting up any formal system; like a Turing machine. Therefore, if you're right that:

The existence of such "component of choice" points to the fact that the body of statements, i.e. the discipline, is in fact not legitimate knowledge. — alcontali

all derived theories from the formal specification of computability are not legitimate knowledge.

EG: We can stipulate that we could equip a Turing machine with an oracle (a black box that allows you to output the correct result from whatever procedure you specify, even one which is undecidable) and derive another concept. This produces a useful theory in studying decision problems.

But why accept Turing machines without oracles vs Turing machines with oracles for your computability definitions? You can arbitrarily stipulate either.

The crux of the issue is that the axiom choice isn't arbitrary in all senses; it's arbitrary in the sense of setting up a formal system, it's not arbitrary in the sense of setting up a formal system to express an intuition, investigate a system (like a series of chemical equations, an electronic input-output machine like a computer) or describe behaviour in the real world.

The choice between different axiomatic systems for different purposes is not an algorithmic one, it satisfies different constraints (useability, prediction, interest, describes stuff well) and is not therefore "merely subjective".

Aah, so I can stipulate {alcontail is wrong about the significance of axioms to justifications in natural language} and derive that and have it be true because axioms are arbitrarily stipulated and nothing more can be said. Right?

It's even computably verified, just restate the axiom.

The example in the last post of "eats" is a blueprint of how functions and predicates are formally constructed and assigned on a domain.

Properties are assigned to lists. EG: "even" = {0,2,4,6,8,...}
Relations are assigned to lists of pairs: EG: "eats" from the last post.
...

Restating something: properties and relations are predicates. Predicates are assigned a number called an arity, which tells you how many things go into them. Properties have arity 1, relations have arity 2. Predicate logic allows you to deal with predicates of arbitrary arity.

Properties are assigned to lists of single objects (arity 1 predicate, list of single elements)
Relations are assigned to lists of pairs (arity 2 predicate, list of paired elements)

This pattern continues indefinitely.

Properties are assigned to lists of single objects (arity 1 predicate, list of single elements)
Relations are assigned to lists of pairs (arity 2 predicate, list of paired elements)
Predicates with arity three are assigned to lists of triples (arity 3 predicate, list of triples)
Predicates with arity x are assigned to lists of x-tuplets (arity x predicate, list of elements of length x).

Functions are constructed similarly.

The function f(x)=x+1 on the natural numbers is exhaustively determined by the list:

1->2
2->3
3->4
...
n->n+1
...

This can be rewritten as the list of pairs
{1,2}
{2,3}
{3,4}
...
{n,n+1}
...

And then aggregated into a single object as with predicates

{ {1,2}, {2,3}, {3,4}, ... , {n,n+1}, ... }

A function of two arguments: f(x,y) = x+y works like

(1,2)->1+2->3
(3,4)->3+4->7
...

Equivalently
{1,2} -> 3
{3,4} -> 7
...

Which is rewritten as:

{1,2,3}
{3,4,7}
...

The number of arguments a function has is also called its arity. A function of arity n is associated with a list of elements of length n+1, representing the n inputs in order and then the output as the last element.

It is convenient to have a structure which compiles all the objects types: "lists of single elements", "list of pairs", "list of triples", ... , "list of x-tuples" together. This is called a Cartesian product .

A list of pairs of all pairs of elements from a domain $U$ is written as the Cartesian product $U \times U$.

A list of all triples of elements from a domain $U$ is written as the Cartesian product $U \times U \times U$.

And so on.

Generally:

A predicate $P$ of arity $k$ on a domain $U$ must be assigned to some subset (sub-list, some part) of the Cartesian product of $U$ with itself $k$ times.

Functions are similar, but more constrained:

A function $f$ of arity $k$ on a domain $U$ must be assigned to some subset (sub-list, some part) of the Cartesian product of $U$ with itself $\mathbf{k+1}$ times. Additionally this subset must satisfy the property that each element of $U$ Cartesian product-ed with itself $k$ times occurs once in the subset (every input list must produce a unique output - a unique term of $U$).

The existence of such "component of choice" points to the fact that the body of statements, i.e. the discipline, is in fact not legitimate knowledge. — alcontali

How do you decide what goes into an "axiom pack"? @alcontali

Let's look at an example, this will contain how we assign predicates meanings (what predicates formally mean) in a simple example, and how we specify a signature and prove theorems about it.

Consider the domain:

FOODWEB={grass, sheep, wolves}

we are going to assign these words to their usual meanings; grass, sheep, wolves.

And the relation "eats" as it applies to FOODWEB.

sheep eat grass
wolves eat sheep

We can characterise the relation "eats" as the collection of pairs:

{sheep, grass}, read "sheep eat grass"
and
{wolves, sheep}, read "wolves eat sheep"

We then collect all the pairs into a single object:

{ {sheep, grass}, {wolves, sheep} }

This is what we assign to "eats" to flesh out its meaning.

So the assignment of "eats" is { {sheep, grass}, {wolves, sheep} }.

The signature is then {FOODWEB, eats}

FOODWEB is assigned to {grass, sheep, wolves}
eats is assigned to { {sheep, grass}, {wolves, sheep} }

We can prove theorems about FOODWEB now.

Theorem: "nothing eats wolves"
Proof: Let x be in FOODWEB, then x is grass or x is sheep or x is wolves (definition of FOODWEB)
A (Disjunct 1) Assume x is grass, then x does not eat wolves (definition of eats)
B (Disjunct 2) Assume x is sheep, then x does not eat wolves (definition of eats)
C (Disjunct 3) Assume x is wolves, then x does not eat wolves (definition of eats)
D (Disjunction Elimination) Then x does not eat wolves (disjunction elimination/proof by cases). (using lines A,B,C).
E (UI) Since x was arbitrary, then for all x, x does not eat wolves (line D, universal introduction/universal generalisation, introduced in thread here).

What this shows is that {FOODWEB,eats} $\vDash$ "nothing eats wolves".

In this case, the entailment is semantic because it follows from the assignment (and the logic rules assumed in the background).

We could turn question around: "find a signature and an assignment in which nothing eats wolves is satisfied", and in that case we find that {FOODWEB, eats} with the above assignment works. This is how models work for first order logic - {FOODWEB, eats} models the claim "nothing eats wolves".

There are other domains and assignments that satisfy this! {grass, wolves}, {sheep, wolves}, {vegetarians, sheep}... with the usual meaning of "eats". It is rare that if we start off with the theorems we'd like, that there is a unique model which satisfies the theorems.

We're going to start talking about the semantics of first order predicate logic now, and relate it to the syntax. In propositional logic, the semantics was all about setting out how well formed formulae are true or false by providing an interpretation of all the logical connectives and constituent propositions; an assignment of true or false to each individual proposition which partook in the well formed formula.

Last post we saw that the overall behaviour of a first order theory depends on the function symbols and predicate symbols and their stipulated relationships; eg how the natural numbers work with addition alone vs how the natural numbers work with multiplication alone; and in this regard, all the function symbols and predicate symbols need to have an interpretation.

To set out the building blocks of a first order theory, a device called a signature is used. A signature has the following symbolic components:

SYMBOLS (SIGNATURE, SYNTAX)
(SIGNATURE 1) A collection of constant symbols.
(SIGNATURE 2) A collection of function symbols
(SIGNATURE 3) A collection of predicate symbols..

Everything which goes into the syntax of a first order theory is a labelled element of a signature, except for the assumed logical connectives, quantifiers and variable symbols. We can also stipulate behaviour for the constants, functions and predicates.

An example is:

$\{\mathbb{N},+\}$

which has the set symbolised with $\mathbb{N}$ of constants (which are intended to be natural numbers) and the function symbol $+$ (which is intended to be addition). If we stipulate that the set is the natural numbers and + is addition - assigning the symbols with their usual meaning - this becomes the usual natural numbers we're familiar with and the usual addition we're familiar with and we can write things like 1+1=2 in the language. Such an assignment is how a first order formal language obtains a syntax!

MEANING (ASSIGNMENT, SEMANTICS)
(ASSIGNMENT 1) A collection of constants - called the domain.
(ASSIGNMENT 2) A collection of functions - called functions on the domain.
(ASSIGNMENT 3) A collection of predicates - called predicates on the domain.

Variable symbols can also be included, but behave differently.

An interpretation of a first order theory takes each element of the signature (SYMBOLS) and associates it uniquely (assigns it) with a part of the assignment. Constants symbols go to constants, variable symbols go to a range of constants, function symbols go to functions, predicate symbols go to predicates.

All an interpretation of a first order theory does is associate all the parts of the signature list to a unique part of the assignment list. Note that there are variable symbols but no part of the signature has variables in it, so variables require a slightly different treatment.

The distinguishing feature of variables is that they can be reassigned to other constants. This range of assignments is what makes them variable. Their labels don't matter very much. EG "For all natural x, x is either prime or composite" means just the same thing as "For all natural a, a is either prime or composite". For any formula, you can replace a variable label with another variable label and not change the meaning of the formula so long as the variables belong to exactly the same object. EG, "for all a, a is either prime or composite" might be false if for some reason we've specified that the symbol a must be a fraction. The intuition this embodies relates to the basic behaviour of the two quantifies:

(1) For some x P(x) is true when and only when we can assign x to some value a and P(a) is true.
(2) For all x P(x) is true when and only when all assignments of x have P(x) as true.

The difference between variables and constants, then, is that variables are defined relative to their ability to be reassigned other elements of the domain and constants cannot be reassigned. The number 2 is the number 2 is the number 2, the number x is... well whatever x could be. The only important thing for using variables appropriately is to use them consistently once you've introduced them.

Setting out how variables, constants, functions and predicate SYMBOLS associate with the ASSIGNMENT list sets out what variables, constants, functions and predicates mean in the language! And once we've set up what they all mean; once we've assigned all the (non-variable) symbols to a unique part of the signature; we can begin looking at what is true and what is false in the language.

Fixed, thank you.

And you? — jgill

Statistics! This is all very pure for me.

The bare bones rules of propositional logic and first order predicate logic are quite similar; first order predicate logic just expands on or rewrites the rules of propositional logic.

A propositional logic argument, modus ponens, detailed here goes like:
$P \implies Q, \hphantom{..} P \vdash Q$
"If P then Q, P, therefore Q"

Much the same thing in predicate logic is:

$P(x) \implies Q(x), \phantom{..} P(x) \vdash Q(x)$
"If P holds of x this implies Q holds of x, P holds of x, therefore Q holds of x".

Similar structures apply for conjunction, disjunction etc:

EG:

(Conjunction Elimination) $P(x) \cap Q(x) \vdash P(x)$ and $P(x) \cap Q(x) \vdash Q(x)$
(Disjunction) $P(x) \cup Q(x)$ implies $P(x) \cup Q(x) \vdash P(x)$ or $P(x) \cup Q(x) \vdash Q(x)$



where $\vdash$ works as before (but now with the well formed formulae of first order predicate logic).

There are also rules for quantifiers: universal instantiation and universal introduction - which define how for all $\forall$ works and existential instantiation and existential introduction - which define how $\exists$ works, these read:

$\forall$
(Universal instantiation) For every well formed formula $\phi$, $\forall x :\phi x \vdash \phi c$ for every $c$ in the domain. This says "if a statement holds of everything, it holds of each particular thing".
(Universal introduction) If for the well formed formula $\phi$ involving arbitrary variable $x$ holds/is stipulated , then $\forall x :\phi x$
This says "if a statement holds of each particular thing/an arbitrary thing, then it holds for everything".

$\exists$
(Existential instantiation) If $\exists x: \phi x$ then in particular $\phi c$ for some c in the domain. This reads "if a thing holds of something in the domain, it (at least) holds of a particular we can label as c".
(Existential introduction) If for some constant element of the domain $c$ some well formed formula $\phi$ holds/is stipulated, then $\exists x: \phi x$ holds, where x is a variable. This says "if something holds of a specified particular thing, it holds of something in general".

The rules for quantifiers also include two descriptive notions which are important; free and bound variables. A variable occurrence is bound in a well formed formula if some quantifier acts on it in that well formed formula and free otherwise. EG

$P(x) \implies Q(x)$ has $x$ free.
$(\forall x P(x) ) \implies Q(x)$ has $x$ bound in the first part and free in the second.
$\forall x (P(x) \implies Q(x))$ has $x$ bound alone.

Only well formed formulas where every variable is bound can evaluate unambiguously to true or false; otherwise they depend on the variables instantiating the claim. Well formed formulae solely involving constants need not be bound in this manner to be true or false. EG:



"Socrates is a man" is true when speaking of philosophers since Socrates is a fixed term of the domain of philosophers and is a man.
"x is a man" might be true or false when speaking of philosophers, because x might be Elisabeth Anscombe who is a fixed term of the domain of philosophers and is a woman. In this case x is free.
"There exists an x such that x is a man" is true when speaking of philosophers because (at least) Socrates exists. In this case x is bound.
"Every x is a man" is false when speaking of philosophers because (at least) Elizabeth Anscombe exists In this case x is bound.

Expressions involving constants and variables at the same time are common, eg:

"For all natural numbers x, if x is even and x is prime then x = 2"
the constant 2 shows up, the variable x shows up, the predicate symbols "is even" and "is prime" show up, all variables are bound so this statement is either true or false, and it turns out to be true since 2 is the only even prime.

Given all this, we can weave the inference rules (this post) and the predicate/function behaviour together to start talking about formal semantics of first order logic; theories and models of stipulated function/predicate rules.

This is, finally, when we get to start talking about axiomatic systems like the Peano Arithmetic and ZF( C ).

Let's stop to consider the richness of the language of first order logic, the kind of things that we can express with it.

(1)"Every number has a prime factor"
$\forall n \exists x : (x|n) \& P(x)$
where | is "divides" and P is "is prime" and & is conjunction.
(2)"There is no largest prime"
$\forall p \exists q: q\gt p$
where p and q are prime numbers and $\gt$ is greater than.
(3)"Every fraction can be multiplied by some other fraction to obtain the number 1 and that fraction is unique"
$\forall x \exists y : (x \times y = 1 \hphantom{...} \& \hphantom{...} \forall z : x \times z = 1 \implies z=y)$
where x is a fraction, y is some other fraction, $x \times y$ is a function term which corresponds to multiplication.
(4) "If a is on the same landmass as b, and b is on the same landmass as c, then a is on the same landmass as c"
$\forall a \forall b \forall c:\hphantom{...}R(a,b) \& R(b,c) \implies R(a,c)$
(5)"$\forall a \forall b \forall c:a \times (b+c) = a\times b + a\times c$"
(the distributive law of multiplication and addition).



One trick here is that things like $+,-,\times$ above are functions; f(x,y) = x+y, if you input x and input y, you get x+y out, so f(1,2)=1+2=3. Subtraction and multiplication work similarly. All the elementary operations in mathematics can be inputted into a first order language as function symbols of their argument terms, and their output interpreted as another term!

Within the above statements, there is an implicitly assumed domain in the background and an implicitly assumed interpretation of the function and predicate symbols.

Regarding the domains: in the first statement, the domain is the numbers 1,2,3,4... . In the second statement, the domain is the primes 2,3,5,7,... . In the third statement, the domain is the fractions. In the fourth statement, the domain is the landmasses (of Earth). In the fifth statement, the domain is something like the naturals or fractions or reals where multiplication and addition interact.

Regarding the function and predicate symbols: in each of these cases, the formal language requires extra symbols to augment the domain with to make sense of the statement. In the first, we add a binary predicate (relation) symbol | for "divides" and a unary predicate (property) symbol P for "is prime". In the second we add a relation symbol $\gt$ for "greater than". In the third we add the multiplication symbol $\times$. In the fourth we add the relation symbol $R$. In the fifth we add the multiplication symbol $\times$ and the addition symbol $+$.

All of these contexts are very different, but first order logic lets you express things about all of them. In that regard, we need to pay attention to precisely what we're talking about; what domain of discourse and predicates and functions make sense on it, and how those predicates and functions interact. And in terms of formalisation, set out exactly what we're talking about to begin with; have an interpretation in mind, an intended semantics.



Due to the expressive power of the predicate symbols and function symbols, we can posit much different structures depending on what predicate symbols and function symbols we augment the domain with. For an example, consider the natural numbers equipped with addition; the only statements which make sense in this context are natural numbers added together and equations between sums of natural numbers. Like 5+2=3+4=7, or "if 5+2 = 3+4 and 3+4 = 7, then 5+2=7", but no statements including multiplication.

If we then add multiplication to this "natural numbers with addition" structure, we can start talking about equations involving addition and multiplication.

This is to say, while in propositional logic, the system of inference (the theories of propositional logic) depended entirely on the logical structure of argument (the valid ways of using logical connectives between elements of he domain), the theories of first order logic depend on stipulated rules of functions and predicates as well as the rules of propositional logic + quantifier rules.

I'm a mathematician who studied a decent amount of logic. The material I've presented here is recapitulating stuff from 2 undergraduate courses in logic. I've checked Stanford Encyclopedia of Philosophy, the Internet Encyclopedia of Philosophy and Wikipedia on what I've written to make sure what I've written isn't completely insane.

Your friend might want to study "natural deduction", "first order logic" and "formal languages".

The rules of the formal language of first order logic tell us how we can build up well formed formulae out of symbols, and what symbols there are.

So we need to specify what the building blocks (called terms) of predicate logic are:
(T1) An alphabet of symbols; here called variables. Every variable is a term. EG, x,y
(T2) Functions on those symbols: eg, if x and y are variables, then P(x,y) is a term. This holds for every function independent of the number of things that go into it, eg Q(x,y,z)... All of these function expressions are terms. Functions without any arguments are called constants, and these are also terms.



Functions take terms and map them to other terms. They are like replacement rules in in the first post. They take an input and produce an output. EG the function defined by $f(x)=t$ takes any input $x$ and produces the term $t$.

These define the objects of the theory of predicate calculus; the alphabet which its well formed formulae will be written with.

On top of these term notions we need well formed formulae notions; ways of producing well formed formulae given other well formed formulae, like with propositional logic and TOY in the first post.

(W1) If $P$ is a predicate, then $P$ of it arguments is a well formed formula. EG if P is "is prime" and x is "2" then P(x) is a well formed formula. EG if D is "divides" and x is 2 and y is 4, D(x,y) is "2 divides 4". As before, D(y,x) is also a well formed formula, it just happens to be false.

(W2) If $x$ and $y$ are terms, then $x=y$ is a well formed formula.

(W3) If $x$ is a well formed formula, so is $\lnot x$.

(W4) If $f$ is a binary connective and $x$ and $y$ are well formed formulae, then $f(x,y)$ is a well formed formulae.

(W5) If $g$ is a formula and $x$ is a variable in it, then $\forall x g$ and $\exists x g$ are well formed formulae.

These set out the basic grammar; the rules of well formed formula production in predicate logic. An example sequence of produced well formed formulae is:

$x=y \rightarrow \forall x (x=y) \rightarrow \exists y \forall x (x=y) \rightarrow ( \exists y \forall x (x=y) )\cup (x=y)$

Where x and y are terms. This uses W2, then W5, then W5, then W4 with $\cup$ for logical disjunction.

Function terms let us write things like:

$\forall x L(x,f(x))$

For things like "every number x is less than f(x)=x+1" with L(x,f(x)) being x is less than f(x).

Note; the only things which can be quantified over to produce well formed formulae are variables in formulae, not predicates or function symbols. This is what makes the predicate logic first order; first order means quantification only over terms (term symbols), not over predicates applied to terms (predicate symbols).

EG: "All colours are sensory properties of objects" is not a first order statement, since colours are properties. Whereas "all natural numbers have at least one number which is larger than them" is a first order statement, as the "all" works on natural numbers and the "at least" also works on natural numbers.

It remains, again, to build a system of inference on top of these grammatical rules of the formal language.

One of the major reasons we need to add quantifiers to a formal basis of mathematics is that we need to be able to deal with infinite domains of objects, and to stipulate properties of those objects. "Every natural number greater than 1 has a prime factor" could only be formulated within the language if we were able to talk about "every number" at once. If we had a system like for propositional logic, "Every natural number greater than 1 has a prime factor" might be rendered like:

2 has a prime factor.
3 has a prime factor.
...

We'd need to do that infinitely many times. This would mean we would need to write down infinitely many statements to formalise extremely elementary properties of numbers. Also, within the statement "has a prime factor" there is another subtlety: a prime factor of a number is a number that is prime that divides the number. IE, "has a prime factor" means "there is some number which is prime that divides the number".

The device which implements the "every number" part of "every number greater than 1 has a prime factor" is called the universal quantifier, written $\forall$ and read "for all". The device which implements the "there is some number" part of the statement is called the existential quantifier, written $\exists$ and read "for some" or "there exists".

There's another element of that statement which we could not render without additional vocabulary; a number being prime, or having a prime factor, is a property of some number. Moreover, say, 12 having 3 as a prime factor is a relation between 12 and 3. Propositional calculus alone does not have the resources to talk about properties or relations, so we need to augment the language with resources for that. We'd like to be able to have a condensed notation that reads "12 has 3 as a prime factor" and "3 is prime" and so on. The latter might be written as $P(3)$, the former might be written as $PF(12,3)$. Generally, these are called predicates; properties, relations, functions and so on.

This means the extra principles that need to be added to propositional logic to be able to implement these kinds of statements are:

(1) Quantifiers, $\forall,\exists$
(2) Predicates: properties, relations, functions etc.

In addition we would like to be able to have all of propositional calculus as valid formulae of whatever language we set up. So this gives us:

Predicate logic = Propositional logic + quantifiers + predicates.

These are required changes in the syntax, and they will induce changes in the semantics appropriate for them. EG: we can't just evaluate a truth table to see if "Every number has a prime factor" is true.

As is the thing-in-itself. — Xtrix

The thing in itself isn't generated by our faculties limits, or anything to do with us, rather it's that which generates whatever appears to us; in order for us to grasp something with a sensible intuition, there has to be a certain movement in the thing in itself that facilitates the generation of appearances in us. The thing in itself being necessary but not sufficient for our appearances.

...though we cannot know (sensibility + cognition) these objects as things in themselves, we must yet be in a position at least to think (thought) them as things in themselves; otherwise we should be landed in the absurd conclusion that there can be appearance without anything that appears. — CoPR

Moreover, it's helpful to mark the boundary between the capacities of our representation and the objects represented. We can have this as a concept without there being any sensible intuition associated with it.

Further, the concept of a noumenon is necessary, to prevent sensible intuition from being extended to things in themselves, and thus to limit the objective validity of sensible knowledge — CoPR

So the noumenon functions as the name of the limit of applicability of sensible intuition; it's about the limit of our subject's faculties; the thing-in-itself is about things conceptualised apart from how they embed in sensible intuition. The distinction between boundary (noumenon) and what lays outside the boundary (thing in itself), what lays within the boundary are phenomena and appearances.

What possible good is it to say that noumena are "for us"? In what way are they for us? Something unknown, whether in reference to our "understanding" or our "sensibilities" or our "capacities for knowledge" are still unknowns and unknowable. They're "intelligible" in the same way, therefore: as unknowns. But that seems to be the extent of it. — Xtrix

In CoPR the noumenon's aligned with what we can experience. But what we can experience isn't coextensive with what is. The noumenon marks the limit of the sensible; the sensibility being a human faculty (or more precisely a faculty of the transcendental subject). The noumenon is the name for that which blocks the co-extension of our faculties (specifically sensible intiution) and being; it's generated through our faculties' limits, as a concept it's about our faculties (a for us). The thing-in-itself is the name for being insofar as it is not conditioned by our faculties; it is that which exceeds the limitations of our faculties. As a concept it's about that which exceeds the limitation of our faculties (it's not a for-us).

So far we built a system of deduction - the rules of inference of propositional logic - on top of a way of writing down grammatical statements within that logic -the collection of well formed formulae of propositional logic -. This was a discussion of the syntax of propositional logic. We then added a formal semantics to propositional logic; a formal semantics was a way of taking well formed formulae and assigning them to a truth value; this was achieved truth functionally, a well formed formula evaluated to true (or false) depending solely on the constituent propositional symbols' truth values and how they fed into the logical connectives. Since the syntax and semantics are formally distinct, this highlights the possibility of a gap between syntax and semantics of a formal language; and this gap is a site of interesting questions.

To discuss these questions with a bit more detail, we need the notion of a theory. A theory is just the collection of derivable consequences from a stipulated set of rules; the collection of all theorems; derivable consequences; of the language. Notably, a theory is closed under the application of the inference rules to its constituents - this means that you can't get extra consequences by applying the inference rules to something which we call a theory.

Accompanying the notion of a theory is the notion of a model; a model of a theory (or of a collection of stipulated well formed formulae and rules) is a collection of objects in which every element of the theory interprets as true.

EG if we have the rule "every element of a set has to have a strictly bigger element", any finite set violates the rule and so is not a model. If we have the rule $A \implies B$, a model of that formula has $A$ false and $B$ true, or $A$ true and $B$ true. Models typically are not unique.

In propositional logic, a model of a formula is just a row of a truth table under which that formula evaluates as true; assignments of truth/falsity to the proposition which make it true. A model of a collection of formulae is an assignment of truth/falsity to propositions which make them all true.

This lets us restate some things: eg $\vDash x$ occurs when every model of propositional logic has $x$ evaluate as true; that is, $\vDash x$ denotes a semantic tautology - something which is necessarily true.


(Soundness) If a well formed formula can be produced through syntactic operations without stipulating any assumptions, is it the case that the semantics will always evaluate such a statement as true? Stated more briefly, is every theorem (syntax) of the system a tautology (semantics) of the system? If something is provable, is therefore true? When this property holds of the logic, it is called sound.

This can be written $\Gamma \vdash x$ implies $\Gamma \vDash x$.

Propositional logic is sound.

(Completeness) If a well formed formula always evaluates as true under every possible assignment of truth values (semantics) to its propositions, is it the case that the system can derive the formula using its rules of inference (syntax)? If something is true, is it therefore provable? When this property holds of the logic, it is called complete.

This can be written $\Gamma \vDash x$ implies $\Gamma \vdash x$.

Propositional logic is complete.

(Consistency) If a collection of well formed formulae can all be true at the same time, then that collection is called consistent. If the theory of a system of inference is consistent, then that theory is consistent.

This can be written: not $\Gamma \vDash \perp$ where $\Gamma$ is a theory. Conversely, inconsistency says "no model exists for this theory", and "its elements can't be jointly true together/satisfied".

Propositional logic is consistent.

(Decidability) Does an algorithm exist that lets you check whether an arbitrary well formed formula of propositional logic belongs to the theory of propositional logic?

Propositional logic is decidable.

These are all nice properties to have, but we still couldn't write an argument like:

"Every number has a square, therefore two has a square".

We're missing quantifiers, and just by introducing them we gain a lot of expressive power but lose decidability in almost every context of interest for mathematical reasoning. We also complicate the idea of a model; "every natural number has a square" must range over infinite collections - the truth table method of checking whether something is a tautology just won't work any more.

All I really intended us to do was to dramatically state the conclusions of each step — Pfhorrest

Fair. Would you be interested in doing the more detailed version I had in mind?

rigorously prove every step of the process — Pfhorrest

It is likely that we imagine different things by rigorous proof. To me, what I've written is still highly informal and suggestive.

It's not just about them being weak or strong though, it's also about the extent to which they are likely to facilitate or oppose your interests. — Baden

Yes, that's well put. Weak/strong is a silly way of saying nothing relevant.

Whose interests would be facilitated by an armed conflict between America and Iran? And would they be facilitated better through this than through other means? Those are much better question framings.

I can't plot a positive economic or strategic outcome to this for the US ruling classes that beats sticking with the Iran deal and encouraging progressive forces in the country. — Baden

If it happens, it's probably imagined as being to the benefit of some of them and not others? Can't say to who though. Weakening Iran through military conflict probably has the same strategic goals as weakening them through economic sanctions, says the largely uninformed me. I have no idea what goes on in the boardrooms.

If/when it happens; Saudi ruling class might gain from destabilised Iranian economy, Israeli ruling class might gain as Iran and Israel have been proxy fighting and economic competitors for various reasons for ages, American ruling class might gain due to its ruling classes's interests being aligned with the Saudis' and Israelis'. Turkey and Syria are in there too probably (Kurdish conflict and Syrian proxy conflicts). If it happens it's not particularly out of the blue, it's more proxy wars and economic conflict between coalitions of nations realising into overt armed conflict between two coalition members.

Considering how much of a staging ground the middle east is for global conflict who the fuck knows what the strategic aims of the conflict would be and exactly what interests in America it would serve.

Feel free to intervene in the bits I've written to add further detail if you like.

with as little as possible and then build everything up from there — Pfhorrest

Define the hand wave operator H as a function on the cartesian product of the axiom set of a formal system with its theory... The language with the hand wave operator is equivalent to the language without the hand wave operator when and only when for all axioms A and for all theorems B H(A,B) is true when and only when the system has A implies B as a tautology...

But why make it a focus of interest? — fishfry

I think it's a fetish for parsimony. I vaguely recall that having a single logical connective simplifies proofs and the well formed formulae definitions (you just nand or nor stuff). But I think that this is more relevant if you're ball deep proving things about formal logics than providing an overview of them.

Would appreciate it, if you've read what I've written, to point out bullshit where I've said it.

Thanks, fixed.



The presentation is very non-standard. If and when you've read it I'd appreciate you pointing out flaws and errors as I'm mostly winging it but checking sources to make sure I'm not doing something completely insane.

The one bit I'm already skeptical about is putting in syntactic copies of contradiction and tautology as logical connectives (of 0th order, constants), then feeding them into the semantics to get false and true. I don't think it does anything to the overall logic, despite being redundant. The only place I've used the syntactic copy of the falsehood symbol is in presenting the disjunctive syllogism as an axiom (I think I've seen this somewhere before, Gentzen?).

I'm trying to stress in the presentation that there are a lot of ways to end up in the same place, so I've not defined a system with primitive logical connectives, just let them be whatever.

I'm a lot less competent on the details for quantifiers, so I expect to write many more batshit insaanities if I end up writing that bit.

The previous post gave a sketch of how a formal language; a grammar of well formed formulae; can be augmented with more structure (inference rules) to produce a system of inference. Together these elements specify the syntax of a formal language. Now we can begin to discuss a semantics.

So far we've defined a collection of well formed formulas for propositional logic; then we've defined a bunch of ways of linking well formed formulas together. Now we're going to develop an idea of what it means for a well formed formula to be true or false. Truth and falsity are semantic properties; specifying how they behave over the well formed formulae of a language specifies the semantics of that language.

It's probably strange to consider all the things we've done so far as 'meaningless', insofar as they don't have any formal semantic properties, but nevertheless seem to behave quite a lot like how we reason logically. The trick here is that semantic properties of a formal language and system of inference rules on top of it is a different structure again: we need some way of interpreting what we've done so far.



An interpretation is just a mapping of well formed formulae to true or false. How a well formed formula of propositional logic is mapped to true or false completely determines the interpretation of that well formed formula. Interpretations in propositional logic are done truth functionally. If we have a well formed formula of logical connectives over propositional symbols, how that formula evaluates to True or False is completely determined by what happens when its propositional symbols are True (T) or False (F)

These are typically spelled out with truth tables for the primitive logical connectives. A truth table specifies the argument propositions on the left and the formula containing them on the right, the truth values on the left lead to the truth value of the well formed formula on the right. For example, $\cup$ and $\implies$.
$\begin{array}{c|c|c}A & B & A \cup B\\T &T&T\\T & F & T\\F& T & T\\F& F & F\end{array}$

$\begin{array}{c|c|c}A & B & A \implies B\\T &T&T\\T & F & F\\F& T & T\\F& F & T\end{array}$

The truth value of a complex formula is defined as the truth value obtained by iteratively evaluating all its logical connectives from the propositional symbols up. EG for $(A \cup \lnot B) \implies (B \implies A)$, we set out all the combinations for $A,B$ evaluate $\lnot B$ as a function of $B$, then use that to evaluate $A \cup \lnot B$. We then evaluate $B \implies A$ as a function of $B$ and $A$ and then finally the whole thing. If you do this as an exercise, you should see that it's always true.

Two well formed formulae are semantically equivalent when and only when they evaluate to the same truth value on every single assignment of truth values of their constituent propositions. A well formed formula which always evaluates as true is equivalent to $\top$, a well formed formula which always evaluates to false is equivalent to $\perp$.

A well formed formula which always evaluates as true is called a tautology, and if a collection of propositions linked by logical connectives - an element of the propositional logic $x$ - always evaluates as true under every truth value assignment, we write ${ } \vDash x$. This is read "the system (propositional logic) semantically derives x". In contrast, $\vdash$ from the previous posts is read as "syntactically derives". This is a distinction between "if this is true then that is true" (semantic entailment) and "if this is produced then that is produced" (syntactic entailment).

I believe this is quite perverse, but I think it serves the point of hammering home the wedge driven between syntax and semantics which we're beginning to bridge; we can write:


$\begin{array}{c|c}\perp & F\end{array}$

$\begin{array}{c|c}\top & T\end{array}$

Since $\perp$ and $\top$ were syntactic elements, we still need to interpret them to true or false. Even though we've set them up to behave just like true and false, and to represent tautologies and necessary falsehoods when appropriate in the syntax, we still need to map them to their semantic analogues to complete the picture; that is, to provide a means of interpretation for all our well formed formulae.

It's easy to lose track of why the truth tables were introduced; so I'll spend some more words on it. When we're setting up a logic, we want to ensure that if we what we assume is true, what we can produce from it is true. "What we assume" is a well formed formula, "is true" is stipulated by assuming it, "what we can produce from it" are the inference rules applied to the well formed formula. It would be nice if all these notions coincided, but it is not guaranteed to hold.

So it is an open question, given the interpretation of symbols, whether we can produce all and only true well formed formulae given the use of the inference rules. The constructions are quite different, no? We have a bunch of rules that produce well formed formulae, and we have a way of assigning truth values to well formed formulae - do the inference rules play well with the truth value assignment? What are the relations between syntactic and semantic derivation in a logic?

These are important questions to answer for a logic. The possible gap between what is true statement of the system - the well formed formulae which evaluate as true - and what well formed formulae the system can produce through the inference rules is the site of the famous incompleteness theorems. This gap is closed by a few properties, soundness, completeness, consistency, compactness and decidability which are necessary for a logic to behave in all the ways we pre-theoretically expect, but famously completeness and consistency together are guaranteed not to hold for almost all mathematical structures of interest (with a classical logic).

To discuss these issues in more depth, we need to introduce the idea of a model and relate it to the truth value assignments. The idea of a model of a system of axioms and inference rules will turn out to be how we can turn a constructed object in the language into an object that behaves how we specify with the specification of axioms (using the inference rules).

To equate the subject with a "mind" is a different topic. — Xtrix

The kind of discussion that distinguishes a mind from a subject is already a more interesting idea than the usual elision of reason which joins them.

Edit: eg, subject as a universal constitution with its own phenomenological structure, a system in which conditions of possibility of experience make sense as an idea (ontological account), mind as particular concretion of that phenomenological structure which learns and experiences within the constraints of its constitution (ontic account) and thereby can discover the universal constitution through logical introspection.

Not that I buy that idea in the edit either, but at least it's got more meat to it than things like "you can't base metaethics on emotion, it's subjective!" or "physical theories are objective, anthropological theories are subjective" or "the warmth of a flame is subjective, whereas its temperature is objective". Or "materialism doesn't make sense because theories are subjective - the object is just a subject's apprehension of the object!"

It may not seem to matter, and it's often hard to care when modern science is so successful -- especially in terms of technology -- but the philosophical underpinnings are still worth questioning. I started this thread to see how many still question this particular notion, and as you can see, not many really do -- yourself included. That's interesting. — Xtrix

I don't give much weight to the distinction, at least whenever I think it's relevant. I think that it generates intractable access problems (how does a mind move a body?); and the conceptual distinction between a subject and an object is still something which has to come from somewhere - why do these entities operate as if there's a subject object distinction and not others? I think it makes more sense to start from a metaphysics of events and interactions (like a process metaphysics) and build up minds and bodies (or subjects and objects and their transcendental structure) out of those than read things in terms of the subject object distinction.

Though I do think it makes sense in terms of a folk psychology construct; something like that it can be a valuable part of our manifest image but when it's treated as foundational or a given it occludes more than it helps.

It seems to be the philosophical basis for modern science, at least since Descartes. — Xtrix

The subject object distinction is a metaphysical distinction; it makes sense when you have an account of souls separated from objects, or minds separated from worlds, mental separated from physical, primary separated from secondary quality and so on. To my mind, to say that the subject object distinction is part of the philosophical basis of modern science is very greedy, as scientific theories and styles of inquiry which produce them only interface with the subject object distinction as part of their intellectual heritage; and as we know, being in the intellectual heritage of a topic does not say anything about being conceptually foundational for or logically consistent with the topic.

I think it's more accurate to say that scientists will articulate justifications for scientific inquiry in the abstract in terms of something resembling the subject object distinction based on how common and pervasively applied a metaphysical intuition it is, rather than saying anything about whether the subject object distinction is really relevant to their work.

Now that we've set up how to specify a formal system to produce strings given a set of production rules and symbol primitives; a formal language; we need to speak about what it means to make a system of inference out of a formal language.

People more familiar with the material will probably be trolled extremely hard by my cavalier attitude to equality and the formal status of arguments, but I hope that it provides enough of a flavour of logic to proceed from. I'm happy to receive comments/criticisms/corrections and rewrite things to be more formally valid, but only if the corrections don't sacrifice (or even improve!) the post being intuitive and introductory.

For a given formal language, we can construct the collection of all possible well formed formulae that can be produced from it. This collection of well formed formulae is the vocabulary with which we will express a system of inference on such a formal language.

For the propositional calculus, the set of well formed formulae is obtainable through the following rules:

An alphabet of propositional symbols.
An alphabet of logical connectives on those propositional symbols - this is like negation, implication, and, or, xor and so on.
(1) Every element of the alphabet of propositional symbols is a well formed formula.
(2) If $x$ is a well formed formula, then $\lnot x$ is a well formed formula.
(3) If $x,y$ are well formed formulae, then $f(x,y)$ is a well formed formula, where $f(x,y)$ is any binary logical connective (like or or and).

$\lnot$ is negation.

We want to augment this language with more rules of a different flavour; a more restrictive collection of ways of linking well formed formulae that embeds intuitions regarding demonstrating propositions given assumptions - deduction proper - rather than constructing new grammatically sound propositions based on old ones. We need to know more than the lexicology of a language to be able to reason using it.

To reason formally using a language, the first step is to formalise and stipulate the rules by which well formed formulas can be reasonably linked to others. These formalised stipulations embed intuitions about what a system of inference should be able to do.

What this entails is letting some variables range over the set of well formed formulas defined above, then stipulating linking statements between the variables using logical connectives. Stated abstractly, it isn't particularly intuitive, so I'll proceed with (some of one way of doing) the specifics for propositional calculus.

All of this is still spelling out the syntax language, so we're still discussing (1) in the previously linked post.

In an introductory symbolic logic class, you'll be introduced to a natural deduction system and asked to prove things in it. This is going to be a very abbreviated form of that.

We're going to introduce a few more rules that allow us to produce well formed formulas given other well formed formulas; except these encode inference rather than grammaticality, these are not an exhaustive list. Given that $x$ and $y$ are well formed formulae of the language of propositional calculus, we introduce some axioms to relate them inferentially.

(some) Inference Rules:

Conjunction (how $\cap$ "and/conjunction" works):
(CE1) $x \cap y$ lets us produce $x$
(CE2) $x \cap y$ lets us produce $y$
(CI) If we have $x$ and $y$, this lets us produce $x \cap y$.

These just say that if two things can be assumed together independently, this means that we can conclude each of the things independently from assuming them together. "There are 2 apples and 3 pears on this shopping list" therefore "there are 2 apples on this shopping list" and "there are 3 pears on this shopping list". These are called conjunction elimination (CE1 and CE2) and conjunction introduction (CI).

Modus ponens (how $\implies$, "implication" works):
(MP) If we have $x$ and we have $x \implies y$, then we can produce $y$.

This tells you that implication lets you transmit assumptions into conclusions whenever those assumptions imply those conclusions.

Now we have to introduce two symbols, $\top$ and $\perp$, which are logical constants (0th order logical connectives)... They will suspiciously resemble true and false respectively for good reason.

Disjunction (how $\cup$, "or/disjunction" works:
(DI) If we have $x$, we can produce $x \cup y$
(DS) If we have $x \cup y$ and $x=\perp$, then we can produce $y$

Informally - since we've not introduced truth or falsity as notions yet - the first says that if we know something is true, we know that either that thing is true or something else is true (which might be quite silly depending on the context, but it's fine here. "1+1=2 therefore 1+1=2 or Santa exists", it's rather artificial from the perspective of reasoning in natural language. The second says that if we know at least one of two things is true, and one of those things is false, then we know the other is true.

A common feature of all these rules is that they have an "if, then" form, given a bunch of inputs, we can produce (a bunch of) outputs. They are production rules that work on well formed formulae that capture a notion of inference. If we have a bunch of inputs $\Gamma$, and they let us produce the conclusion $\phi$, we write $\Gamma \vdash \phi$. The distinct elements of the bunch of inputs will be separated with commas (and canny readers will probably notice that comma separation before $\vdash$ does exactly the same thing as making a conjunction of the separate elements).

As a sample of how to use this notation, we can write out some rules involving negation:

(DNE) $\lnot \lnot x \vdash x$
(PBC) $x \implies \perp \vdash \lnot x$

These say "not not x lets us produce x" and "if x implies the falsehood symbol, then we can produce not x". Rephrasing them (informally at this point) in terms of truth and falsity. If we know that not X is false, then X is true; this is double negation elimination (DNE). The second one says that if x implies a falsehood, we can conclude that x is false, this is proof by contradiction.

Some curious features of the formalism are that we don't need to stipulate anything at all to derive (anything which is equal to) $\top$, IE $\{\} \vdash \top$ (this is writing that there's no premises to the argument, and that the system derives the conclusion with no stipulations). And that if we start with (anything which is equal to) $\perp$ we can derive anything - $\perp \vdash x$. Any statement which is provable from no assumptions is called a tautology (it is equivalent to $\top$ in some sense). The latter is called the principle of explosion.

Two examples of a proofs (using the stated axioms):

We want to show that $\perp \vdash x$.
(1) Assume $\perp$.
(2) $\perp \cup x$ (DI)
(3) $x$ (DS).

We want to show that $A \cap B, A \implies C, B \implies D \vdash C \cap D$:
(1) $A$ (CE1)
(2) $B$ (CE2)
(3) $C$ (using $A \implies C$ and MP)
(4) $D$ (using $B \implies D$ and MP)
(5) $C \cap D$ (3,4, CI).

A canny and sufficiently pedantic reader will have noticed that in each of these proofs I've made assumptions, then used those assumptions to derive conclusions. This is called a conditional proof. But if we're being extremely pedantic about the foundations, even that can't be taken for granted (it either has to be some assumption of the system itself or provable from/about the system).

Formally, this looks like:

(CP) If we have that $\Gamma \cap x \vdash y$, then this means $\Gamma \vdash x \implies y$.
or
$x \vdash y$ implies $\{ \} \vdash x \implies y$.

This is called the deduction theorem, it's what's lets you link the ability to produce a well formed formula using the inference rules to the overall ability of the system to produce that well formed formula as a conclusion.

At this point, notice that there are four things kicking about in the discussion that look a lot like entailment:

(1) The rules that produce well formed formulae from other well formed formulae.
(2) The implication symbol internal to the formal language $\implies$
(3) The statement that the rules that produce an inference from a set of assumptions $\vdash$
(4) Some further sense of entailment that lets us say $x \vdash y$ implies $\{ \} \vdash x \implies y$, the middle "implies"; this is some 'meta theoretical' entailment, as it's entailment about the formal language under consideration.

All of these are formally distinct entities! They aren't the same thing and don't mean the same thing. But when reasoning about mathematical structures, so long as the context is sufficiently clear, we don't need to keep track of all the distinctions; when reasoning about objects that are sufficiently far removed from what spelling out reasoning even means, we don't have to pay so much attention to all the internal distinctions between entailment types.

But for now we do.

Don't know enough about type theory to comment.

No, we'll get to those eventually... if anybody actually plays the game instead of arguing about the premise of it. I mean, I can build you the integers, rationals, reals, and complex numbers in my next post if you like, though I'm not up to building arithmetic out of set operations alongside it, so I was hoping someone else would do that. — Pfhorrest

Might as well start then. I'm largely going to assume that we can have a classical logic in the background with whatever rules we need (so it's non-constructive as in the usual way people do math), and proceed in the less formal manner of mathematical proof. If you want to try to translate the arguments into formally valid ones, give it a go, but you will almost certainly give up when you realise how insane it is to try and prove everything like in a logic textbook.

Beginnings - An Overview Of Some Of The Crap In The Background to Even Get Set Theory Going

Informally, sets are collections of objects.

When you start building up a mathematical theory axiomatically, unfortunately the word "informally" means "a miracle occurs" or "lots of abstractions are at work in the background to make what I'm saying true".

If you want to remove the miracles, the only recourse is formalisation; that is, to specify how to make a structure of elements you can reason about (like propositions), and specify the ways you can reason your way about in the structure (like rules of inference).

Underneath this is a question of the language that you're using - when you no longer take reason's intervention in language for granted, why should you be able to take the language itself for granted either? So you also need to be able to specify exactly the kind of symbols that you're using and how they relate, and what it means to be a statement.

This specification consists of two components:

(1) A formal language (a syntax).
(2) A way of providing interpretations of that formal language (a semantics).

A formal language is a formal system. It consists of a set of symbols that you define a grammar for. Like the symbols in logical arguments: $A \implies B$. You stipulate a bunch of symbols and ways of combining them. The bunch of symbols are building blocks of the language. The ways of combining them are how you build things with them. The bunch of symbols in a language are called primitives, and the ways of combining and replacing them are called production rules.

When you have a formal language, you have a way of combining symbols with other symbols to produce valid formulas in the language. When you apply stipulated production rules to stipulated starting symbols, you end up with a well formed formula. If you mess up, you end up with something that is no longer part of the formal language. Drawing special emphasis - a formal language consists solely of well formed formulas, things which can be built from applying production rules to primitives.

If we have a language consisting solely of:
Symbols: A, B
Production Rules: (R1) Whenever you have a symbol, you can replace it with two copies of the symbol.
(R2) Whenever you have A, you can join B to its right.
(R3) Whenever you have B, you can join A to its right.
(A): We start with A.

We refer to the collection of all these things together as TOY.

We can make sequences of formulae like $A \rightarrow AA \rightarrow AAB$, which starts with A, applies R1, then applies R2 to the second A. But we can never produce BAA, why? Because the only way we can produce formulas requires that the first B is always to the right of the first A. The only way we can introduce a B is by joining it to the right of an A, and we can only start with A. BAA is then not a well formed formula of the language, whereas AAB is.

If we adjoined another rule (R4); that we can reverse any formula and obtain a new formula, we can now obtain BAA. What this highlights is that what counts as a well formed formula of a formal language depends entirely on how you set up the rules for the formal language; you can only get out consequences of what you put in.

For any sufficiently interesting formal system, there will be a gap between what counts as an element of the language and what is a derivable consequence. This is a distinction, roughly, between what is sayable and what is demonstrable. As may be obvious, to furnish this distinction we need a distinction between a well formed formula and a derivable consequence. This ultimately turns on there being a difference between how well formed formulae are produced and how consequences are derived; and this is fleshed out in a distinction between the formal language (like TOY, or the language of propositional logic) and a system of inference on its elements (to be introduced).

So we're going to talk about propositional logic now. Propositional logic has such a distinction; between its well formed formulae and its derivable consequences.

This sets out what it means for a formula to be well formed in propositional logic:

We need an alphabet of propositional symbols.
We need an alphabet of logical connectives on those propositional symbols - this is like negation, implication, and, or, xor and so on.
(1) Every element of the alphabet of propositional symbols is a well formed formula.
(2) If $x$ is a well formed formula, then $\lnot x$ is a well formed formula.
(3) If $x,y$ are well formed formulae, then $f(x,y)$ is a well formed formula, where $f(x,y)$ is any binary logical connective (like or or and).

Analogously to TOY, (1) gives us the set of starting points (any individual propositional symbol) and (2),(3) are the production rules.

Per @Pfhorrest's comment, if you want to be very conservative you can have a single binary logical connective in your domain - nor - and generate all the logical connectives. But from the perspective of building up the larger structures desired in this thread, such parsimony is not required or desirable (IMO anyway).

This is just like TOY, but the rules are different. Let's have an example: denote logical conjunction by $\cap$. A sequence like we built in TOY goes:

$\displaystyle x \rightarrow \lnot x \rightarrow \lnot x \cap x$

This starts with $x$, assumed to be a propositional symbol of the language which is thereby a well formed formula by rule (1), we then apply rule (2), we then apply rule (3) with conjunction and $x$. This well formed formula is "x and not x". Perhaps why it is silly to require every step in a demonstration to be done explicitly with stated rules becomes obvious at this point; it is easy to construct things which are obviously well formed formulae:

$\displaystyle x \cap (y \implies x) \cap \lnot (x \implies (y \cup \lnot z))$

where $\cup$ is logical disjunction, but demonstrating that this is so based off the rules is tedious and uninformative.

If someone wants to start talking about the inferential theory of propositional logic from here that would be fine, if not I'll make the post later.

Someone else please check this because I don't trust alcontali's word on this for various reasons, and my understanding is that from set theory you can build predicate logic, which serves as an extension of propositional logic (anything you can say in propositional logic you can say in predicate logic), so if you start with sets you don't need to "manually" include propositional logic, it's one of the things you can build along the way. — Pfhorrest

You need logical symbols to state set axioms. You also need them for Peano arithmetic (and the Von Neumann version you presented in the OP). You don't have any tools to reason about sets without putting the reasoning system in the background - roughly, positing inference rules to output theorem statements from axiom statements.

With more rigour you need to specify a whole formal language to specify the logical connection of statements, typically a Hilbert system with first or second order quantification, AFAIK you only need first order to specify everything in the plan I posted up until you get to the analytic properties of the reals, in which case in the standard treatment you need second order quantification to axiomatise the completeness property of an ordering (quantifying over upper and lower bounds of a set is a second order logical statement).

Regardless, if you actually try to reason about objects in derived theories (like naturals from sets) using only the set and logical axioms, you'll find that the proofs for every statement get intolerably long, and at that point you switch to natural language and appeal to intuition (which is translatable to the inference rules if you do it right).

It would be fantastic if it were possible to derive the 14 axioms of propositional logic as theorems in ZFC, but I have not run into any documentation that confirms this or clarifies how to do that. I am absolutely not sure that it can be built along the way on top of ZFC. All documentation that I have seen up till now suggests that it is simply another, additional axiom pack. — alcontali

Considering you need to axiomatise the behaviour of quantifiers to state ZF axioms (eg extensionality) or Peano axioms (eg the successor function being injective)... It's kinda redundant to start from sets then derive quantifiers (like for some being arbitrary disjunction over set elements, or for all being infinite conjunction over set elements).

I think there's a big difference between expecting to show how the entire universe works mathematically (what some people seem to be reading the thread as) vs exhibiting one way to go from set theory to the mathematics of physical laws without loads of rigour. The "derive cells from sets" goal is very silly, the "show what math goes into some simple physical laws from the ground up" goal is not.

I'd be willing to contribute to a more modest, though still quite ambitious, project, where we go from say, sets to simple harmonic motion when we can handwave too arduous technical requirements.

We should put the logic in the background then, except where it's completely necessary to go into it. I'm guessing that we'll need to set it up so that binary relations make sense; for equivalence relations in setting up algebraic operations on the rationals and reals and for order relations when we need the ordered field construction and the convergence/continuity/differentiability stuff that relies upon the completeness of the real line.

If you read the OP you’d see that that’s just the midpoint. We build up to something like QFT, and then build from there to something like a human. I’m not specifying the exact route we must take or how far we can go but that’s the rough idea. — Pfhorrest

I don't think you realise how big a project just getting to differential equations of real variables would be. It's a lot of work.

Interested in filling out parts of the story that I know.

1. If you are aiming at some fundamental physics, such as QFT, that still leaves out every non-fundamental theory that is not reducible to fundamental physics - which means pretty much everything, from solid state physics to derivative trading. Now, it is plausible, though still controversial, that, to the extent that they are accurate, those "special sciences" supervene on fundamental physics. — SophistiCat

I was thinking about this issue. If we want to arrive at a general description of... well, everything maths oriented as it pertains to modelling physical systems with deterministic laws, we'd probably need to have extremely abstract foundations. The end result of that would look more like the nlab than an accessible thread on a philosophy forum.

So I propose that whoever wants to fill out parts of the story, we limit the scope and split it into a bunch of subtopics.

Set theory -> Definition Algebraic Structure (DAS) of the Naturals -> DAS Rationals -> DAS reals -> Analytic structure of the reals -> calculus of real functions -> differential equations -> specific examples of physical laws.

Linear algebra (if required) would fit somewhere after the DAS of the reals (the field construction and the vector space over a field construction).

That's a simplified version of the story that misses out a lot; like action formulations of physical laws, complex analysis and Hilbert spaces, which would limit the quantum parts of the story we can tell. We're also missing a more general structure for the calculus and analytic structure of the reals (need more general topological/differential geometric notions) that allow tensor equations to be written.

I bow to your maths knowledge, but I'd still maintain that there is nothing in our universe to which the axiom 'when it is changed, it does not change' applies. — Devans99

I guess it comes down to whether you require that the application of a function to an input necessarily produces a distinct output (IE, no fixed points). Trying to avoid this blocks lots of useful things.

We have changed something and it has not changed. — Devans99

A function can have fixed points. These are when you get the same thing out as what you get in.

The operation "take a sequence, delete every second element, output the sequence without the deleted elements" is a function on the space of infinite sequences to the space of infinite sequences. It has a fixed point (produces an output equal to the input) whenever:

{a1, a2, a3, a4, a5, a6, a7, a8, ...}={a1, a3, a5, a7, ... }

a1=a1, a2=a3, a3=a5, a4=a7...

whenever all sequence elements are equal.

Notably, the sequence {1,2,3,4,5,6,...} of naturals produces the odds {1,3,5,...} upon applying this function. So, applying the function can produce the same thing (when the input sequence is a constant sequence), or produce a different thing (when the input sequence is not a constant sequence).

Again they are in a one-to-one correspondence so they are identical collections. — Devans99

I'm thinking of them as sequences.

The first sequence, the one in your OP, is the sequence "the constant sequence where every element is b".

The second sequence, the second one in your OP, is the sequence "the sequence derived from the previous constant sequence by deleting every second element". This is also "the constant sequence where every element is b" since the sequence consists solely of the constant b... The constant is b, and every element is b.

The two sequences are identical. They also have the same cardinality. They are not identical because they're in a one-one correspondence, they're identical because all their elements are the same and in the same order.