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: Describing models of a theory

Julius Hamilton (Oct 10 2024 at 13:40):

I was wondering if the following is correct.

Let $T_1$ be a theory consisting of the formula “$\forall x [f(x) = x]$”, for function-symbol “$f$”.

In order to determine models for this theory, select a set $S$.

To be valid, “$f$” must be realized as a function $[f] : S \to S$, for which, for all $x \in S$, $[f](x) = x$.

It seems like we are saying the same thing, but we’re not. We’re using concepts from the ambient set theory, when we say:

Let $[f]$ be a function $[f] : S \to S$, such that for all $x \in S$, $[f](x) = x$.

I think there is a formal way to show that if you map $f \to [f]$, then $\{S, [f]\} \models T_1$. I am not sure at this moment what that is. I recall there is an inductive definition of the $\models$ relation, but I think it defines “(a map from a signature to a structure) modeling (a theory)” similar as to above: “$c \equiv d$” iff $[c] = [d]$; “$cRd$” iff $[c][R][d]$. Similarly, it defines the meaning of logical symbols in terms of natural language - for example, $S \models$ “$\forall x [R(x)]$” iff for all $x \in S$, $[R](x)$. Or maybe, iff for all $x \in S$, $[R](x) \models$ “$R(x)$”?

Let’s assume we showed formally that $\{S, [f]\} \models T_1$.

By an abuse of notation, we also say $\Gamma \models \phi$ iff for all models $\mathcal{M}$ of $\Gamma$, $\mathcal{M} \models \phi$.

Again, there is some slipperiness, to my mind, regarding distinguishing between formulae of the theory, versus the language we use to describe our model, to show they link up.

In the language of my ambient set theory, I might say that for all $x$, $f(f(x)) = x$; or that $x = x$, where $f$ is still the function $f : S \to S$ such that $f(x) = x$.

To show that $f(f(x)) = x$ in a model, it seems easier to select a set $S_1$ and use algebraic rules to show $f(f(x))$ reduces to $f(x)$ which reduces to $x$.

I suppose to show that this holds in all models, I should try showing the above, for arbitrary $S$?

Something like:

Let $S$ be any set.

Let $[f]$ be the function $f : S \to S$ such that $f(x) = x$.

Let $J : \Sigma \to \{S, [f]\}$ (where $\Sigma = \{f\}$).

$\{S, [f]\} \models T_1$, because “$J(\forall x [f(x) \equiv x])$” becomes “$\forall [x], [f]([x]) = [x]$” (or roughly that. I recall now there is a notation for expressing this that I will go back to and study now.)

And I suppose I am to say, that since the identity function $f$ on any set $S$ has the property $f(f(x)) = x$, I would be able to conclude that $\forall x [f(x) = x] \models \forall x [f(f(x)) = x]$.

Seeking advice, commentary or discussion. Thanks.

Federica Pasqualone (Oct 10 2024 at 20:09):

Let me first ask a question: are you trying to define a subset in a model or realize a type?

Julius Hamilton (Oct 10 2024 at 21:16):

I didn’t think I was trying to do either of those things, but maybe I was and didn’t realize it.

Federica Pasqualone (Oct 11 2024 at 00:05):

Alright, then! Maybe this was overkill and you're just playing around with substitution.

Julius Hamilton (Oct 11 2024 at 00:08):

I don’t know, but I’d love to hear your thoughts and learn more from you.

Julius Hamilton (Oct 11 2024 at 00:25):

But ultimately, my question is about the proper way to prove that a formula $\phi$ is semantically entailed $\models$ by a group of formulae $\Gamma$.

Federica Pasqualone (Oct 11 2024 at 07:32):

But this is a totally different story, and we do not really need model theory for that!

Federica Pasqualone (Oct 11 2024 at 07:33):

It is sufficient to have a system whose soundness and completeness is proved and a bunch of premises and rules of inference to do the proof.

Federica Pasqualone (Oct 11 2024 at 07:33):

:sunglasses:

Federica Pasqualone (Oct 11 2024 at 13:29):

Call the axiom that you have AX. Now, lucky you, FOL is sound and complete. So the argument goes like this:

1. Fix $x$ any ;
2. Take $f^2\left(x\right)$;
3. By AX: $f\left(x\right) = x$;
4. Thus, $f\left(x\right)$;
5. By AX: $f\left(x\right) = x$;
6. Hence, $x$.

This is the mathematical deduction, then you have to encode it (if you have to idk);

Federica Pasqualone (Oct 11 2024 at 13:30):

Notice also the business works for any power of $f$.