Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: theory: mathematics

Topic: Derivability and Consequence

Julius Hamilton (Jun 09 2024 at 18:32):

I am having difficulty expressing the following question.

In a first-order alphabet, normally, the only things which change from alphabet to alphabet are the symbols in the signature, which is the constant, function, and relation symbols. Therefore, in all first-order alphabets, we still have quantifier symbols, variable symbols, logical connectives, equality, and punctuation, but they have the same meaning/use, from alphabet to alphabet.

Once you can select an interpretation of an alphabet, you can define the satisfaction relation; which conveys Tarski’s conception of semantics. As I see it, Tarski’s semantics aren’t “formal”. They are a way of interpreting the symbols in the alphabet through human intuition. So we say that $\mathcal{J} \models t_1 \equiv t_2$ “if and only if $\mathcal{J}(t_1) = \mathcal{J}(t_2)”$ ; and $\mathcal{J} \models \neg \phi$ “if and only if not $J \models \phi$ ”. It tells you what the logical and quantifier symbols mean.

It almost looks like we are describing the relationship between a set of formulas $\Phi$ and an interpretation $\mathcal{J}$ in natural language - so the meta-language of first-order logic is apparently natural language.

Later, the derivability relation is defined, ‘ $\vdash$ ’. I haven’t learned it yet, but I have an idea that it means a sentence is obtainable through the use of sequent calculus.

With $\models$ and $\vdash$ defined, we can express meta-logical properties of a theory $\Phi$ under an interpretation $\mathcal{J}$ . For example, if $\Phi \vdash \phi$ and $\Phi \vdash \neg \phi$ , $\Phi$ is inconsistent. If $\forall \Phi, \phi, \Phi \vdash \phi \implies \Phi \models \phi$ , $\mathcal J$ is sound (I think).

I want to understand how you could write the above relations as part of a first-order alphabet, whose signature would include $\vdash$ , $\models$ in its set of relation symbols. If the meta-theory of FOL is itself a first-order theory, do we discover something interesting in studying it that way?

Jean-Baptiste Vienney (Jun 09 2024 at 21:08):

There is a question which seems very similar to what you ask here.

Peter Arndt (Jun 12 2024 at 22:26):

I am not sure what you are looking for exactly, but maybe this is interesting for you: In Carnielli, Coniglio: Transfers between Logics and their Applications the authors consider the consequence relations of propositional logics as interpretations of relation symbols of a first order signature.

Ryan Wisnesky (Jun 13 2024 at 04:36):

perhaps you are noticing, like tarski did, that 'truth' in arithmetic cannot actually be axiomatized in arithmetic: https://en.wikipedia.org/wiki/Tarski's_undefinability_theorem . Like, you can't treat |- and |= as though they were just plain function symbols in FOL, because they can't be axiomatized without running into decidability issues

John Baez (Jun 13 2024 at 11:46):

I would expect that derivability, aka provability, $\vdash$ , in first-order logic can be axiomatized in meta-theory expressible in first-order logic. After all we usually have rather simple rules for how to prove something given something else!

It's often only semidecidable when something is provable given something else: that is, we can recursively enumerate the provable statements but not always recursively enumerate the unprovable ones. But this is no obstruction to axiomatizability, in fact it's typical of axiomatic systems once they're powerful enough.

Eric M Downes (Jun 13 2024 at 15:12):

John Baez said:

I would expect that derivability, aka provability, $\vdash$ , in first-order logic can be axiomatized in meta-theory expressible in first-order logic. After all we usually have rather simple rules for how to prove something given something else!

Hear hear!

Like we can build a very stripped-down finite thin abstract category that models provability in FOL. We don't even need sets per se, just some simple data and rules.

What is wrong about this? (It's not formalized, but I think it works)

Data and context.

The external FOL symbols and rules $\top,\bot,\lnot,\land,\lor,\ldots$ with modus poenens
$x\land (x\Rightarrow y)\implies y$
A finite number of "Objects" $a,b,c,\ldots, x,y,z$ AKA predicates
"Arrow" $\vdash$ connects predicates to form a new predicate, one on the left, one on the right.
Formal Containment as a predicate $x\in O; ~~y,z\in O$ just expresses "if $x$ is an object; if $y,z$ are objects" in shorthand. (That is, if they are legal predicates)
3b. $z\in O\implies [x,y\in O\Rightarrow z]\iff [x\in O\land y\in O\implies z]$ makes explicit the meaning in (3), could also go under rules.
We assume $O$ contains at least $\top,\bot$ .

Rules

$\top\vdash(\top,\bot\in O)$ (we can prove things about this system, very weakly)
0': $\lnot(\top\vdash\bot)$ (optional... maybe you want a trivial system!)
$x\in O\implies x\vdash\top$
$x\in O\implies \bot\vdash x$
$x\in O\implies x\vdash x$
$x,y,z\in O \implies [x\vdash y\land y\vdash z\implies x\vdash z]$

We can even express what Julian called "soundness" $\models$ , though we cannot prove much about it:

$x,y\in O \implies[x\vdash y\land \lnot(x\vdash \bot):=(x\models y)]$
where ":=" is a tautology (definition). That is, we ignore any proofs implying $-\vdash\bot$ .

Notice I'm not claiming FOL is inside this system in any way, just statements about $O$ , and the internalization of certain concepts ( $\implies$ is suspiciously similar to $\vdash$ ...) and the (possibly unknown) composition data. These statements become fruitful when you have some rules about what are legal theorems that relate this category to the things you want to use it to express consistently. That is, place more objects other than $\bot,\top$ into $O$ .

This is not novel nor particularly deep. It is just (my memory of) the heyting algebra. I hope it addresses Julian's question, without running afoul of Tarski's theorem.

Julius Hamilton (Jun 21 2024 at 02:54):

I think this paper will be of use: http://www.uni-log.org/SurveyAAL.pdf

Julius Hamilton (Jun 21 2024 at 02:56):

And this: https://en.m.wikipedia.org/wiki/Heyting_algebra

Eric M Downes (Jun 21 2024 at 13:16):

Additionally, here (corrected) is a very accessible series of videos giving an overview of category / HoTT adjacent topics by Richard Southwell. He gets to heyting algebras by lec 4/5. Great for the concepts and big picture of why they are important.