Logic - 2020-09-10

user400188

08:19

@user21820 Do you have any free time? I have a few comments about the answer you posted to one of my questions, but they are too long to put in the comment section of the answer.

user21820

@user400188 Just post it there. If you have a question, it is likely others who read that thread may also have it. Unless you want to discuss something not directly related.

@Cure: What @MaliceVidrine is saying is that pure FOL proves ¬∃R ∀x ( I(x,R) ⇔ ¬I(x,x) ), where I is a binary predicate-symbol.

Similarly pure FOL proves ∀A ( I(A,A) ∨ ¬I(A,A) ). If you do not like that, then you need to dispute either LEM (law of excluded middle) or the idea that set membership is a boolean question.

user400188

They are not questions, just comments. Also, I ended up writing it in the draft question meta post. I could export it here or just post a link. Which would you prefer?

user21820

@user400188 If you're using the sandbox on meta, you should just paste it here, because the sandbox is designed for people to reuse.

user400188

sure

> Firstly, it is not correct to write "$a≠a$" when referring to the element that $a$ is interpreted as in a structure $M$. Either write "$M ⊨ a≠a$" or "$a^M ≠ a^M$.

I wrote in my answer, if we instance $x$ to $a$ in an interpretation where $\forall x\lnot (x=a)$ is true, then we arrive at $a\neq a$, which is contradictory. While I agree that writing $M\vDash a\neq a$ is more precise, one of the reasons it is so, is because it's more specific. If $a$ is a variable or a constant, the assumption of $\forall x\lnot (x=a)$ will eventually lead to $\lnot(a=a)$. If I choose to use the model theo…

> Secondly, it is not a very good idea to prove that it is a tautology by proving that its negation is contradictory in every structure, because this relies on classical FOL semantics, which is unnecessary here. It is always better to rely on only the relevant aspects.

It may be just a nitpick, but in my answer, I proved that it was a valid statement by assuming that its negation was true in *some (not all)* interpretations, and deriving a contradiction from that. If I had instead assumed that its negation was true in all interpretations, then I would have proved a different thing.

Also, I think that classical FOL semantics are relevant here, because they are heavily standardised and well understood. The purpose of the question and answer was to be as clear as possible, and it seems to me that classical FOL semantics is the best way to do it. For this pu…

Sorry about the indentation, I didn't know that ">" would render differently in chat.

user21820

Doesn't matter about format.

@user400188 No that is not correct. If you want to give a semantic proof, you really have to go all the way to the elements of the domain. You cannot stop at "a≠a" which is merely a string in the language.

That is why you either have to write a^M (interpretation of a in M) or you put it under the "⊨" so that it is a semantic claim.

As for classical FOL semantics, it's not the best way to do it because you will take more steps than the way I presented, precisely because you have an extra proof by contradiction wrapper. If your answer looks shorter, it is only because it is missing key steps, which is the point of the above remark.

user400188

08:34

I thought you might say something along those lines. My preference would be to use $a^M$, because that nothing about whether $a$ is a constant or variable.

By the way, is it correct to claim that the proof works for both those case if such notation was used?

@user21820 Judging by this second comment, I guess the proof doesn't work because it is missing steps.

user21820

@user400188 Let's just put it this way: It is more work to rigorously prove that "∃x ( x=a )" is invalid implies "∀x ( ¬(x=a) )" is true in some interpretation, than to just go the direct route as in my answer.

What is happening is that you are using your (correct) intuition to skip over that step, but that gap is larger than the proof of the theorem you want.

user400188

I think the problem here is that I still haven't done a proper model theoretic proof before, and have only made meta logical proofs about FOL with some model theoretic notation/concepts thrown in.

user21820

Yes that is probably the case. So I suggest you study the proofs I gave closely to see that a semantic proof can be done algebraically without any intuition-based words.

user400188

To me, the proof I gave with all the steps skipped seems as rigorous as the direct method you suggest, because I don't know the standard way to do things.

user21820

But you are correct that my proof in two cases can be simplified if you use interpretations instead of structures. I did the structures approach because it has to be done at some point in setting up FOL, whether in proving things like this or in proving the completeness theorem for FOL.

If you want to see that proof: Take any FOL interpretation (i.e. structure plus variable assignment) I that interprets symbol a as a variable or constant. Then I ⊨ a=a, so I[x:=a^I] ⊨ x=a and hence I ⊨ ∃x ( x=a ). Therefore, ∃x ( x=a ) is an FOL tautology.

@user400188 By the way, what I am saying is that you did not prove the implicit claim ( "∃x ( x=a )" is invalid implies "∀x ( ¬(x=a) )" is true in some interpretation ). That is why it is not rigorous. In contrast, there are no missing steps in my answer, given appropriate definition of FOL tautology.

user400188

08:51

I was careful not to use the phrase FOL tautology in my answer, as part of the question was what can and cannot be consider one. Since there is some disagreement on what can be called a tautology, I left it until the end of my answer. (Although FOL tautology is pretty explicit).

@user21820 I am actually quite unfamiliar with the word structure in logic. I have been shown that Hilbert proofs for FOL are sound and complete, which I have interpreted as: there exists a deductive system which is complete for FOL. Which I take as the long hand version of the short hand phrase: FOL is complete.

user21820

@user400188 How do you define "complete for FOL"? There is no way to define FOL semantics without interpretations, and as I said above an interpretation is nothing more than a structure plus variable assignment.

user400188

Instead of structures, I have been introduced to the concept of "model", which consists of a domain and interpretation. The domain is the objects external to the logic which you are talking about, and the interpretation assigns names to objects, and truth values to predicates on names, to be brief.

user21820

Ah.

The term "model" is only appropriate in some situations.

user400188

I think some of the terms have been switched in our two different definitions.

wait never mind, "interpretation" contains what you call a structure. I thought it was the other way around.

user21820

Different authors may use different terms, but conventionally "model" is a relation. In this usage, we can say "M is a model of T", but not "M is a structure of T".

user400188

08:59

I assume it would be correct to say: M assigns a structure to T? (By way of the interpretation it assigns).

user21820

That's right!

To prove semantically that something is an FOL tautology (I'm using it in the same sense as you), we simply quantify over all structures that interpret the symbols. To prove semantically that a theory T logically entails Q, that is T ⊨ Q, we would quantify over all models of T and show that Q is true in every one of them.

Conventionally (myself included) we distinguish between structures and models not only to make such distinction clear, but also because it is structures that appear in normal mathematics outside logic, rather than interpretations (with their variable assignments).

⟨ℕ,0,1,+,·,<⟩ is a structure, for example. And its language is called the language of arithmetic.

user400188

How do we quantify over all models? I also have a similar question for structures.

I think we once proved in this room that we have a name for every object, in every model of any first order theory.

Since models contain names, it appears we are doing a similar thing here. Something has to give, either we are not doing it for all names, or not all FOL theories.

Sorry, that should be: I think we once proved in this room that we cannot have a name for every object, in every model of any first order theory. (I missed the key word)

user21820

09:23

@user400188 Your last statement does not type-check... Models/structures do not have names.

user400188

I know nothing of types in logic.

user21820

I don't mean anything about type theory. It is just that there is no such thing as "names in every model ...".

Ah I get what you meant. Sorry I got tripped by your ambiguous phrasing.

user400188

It was the best I could do with my limited knowledge.

How does an interpretation, which is contained in a model, assign names to objects if those names are not contained in the model?

Also, I have an attempt now at the interpretation based proof you asked for. I'm following my assume this, get contradiction approach.

user21820

Given any first-order theory T with at least one model, there is some model M of T such that some element of M is not the interpretation of every constant-symbol of T.

This is what you're referring to.

However, it is irrelevant to the question we were just discussing, because we are working inside the meta-system.

I strongly suggest you stop using imprecise terms like "names" because they seem to be a frequent source of your confusion.

MS (definition): Q is an FOL tautology ⇔ ∀I ( I is an interpretation ⇒ I ⊨ Q ).

MS (theorem): "∀x ( x=a )" is an FOL tautology.

Obviously, to prove this theorem rigorously, you need to have a proof like this:

Given interpretation I:
  ...
  I ⊨ Q.

I'm leaving out some minor details like the fact that we need to quantify over only interpretations that assign the relevant variables, because that is not important now.

What is important is that you do not seem to realize that you are working within MS and have to use FOL deduction within MS to prove what you want to prove about FOL.

MS can quantify over strings, and can also quantify over interpretations, structures and whatever else. In set theory, a structure is defined as some set such that blah blah ... Similarly, an interpretation is some set such that blah blah. In set theory, there is nothing but sets.

user400188

@user21820 Sorry, I realised my mistake after the 3rd point. I didn't point it out because I was helping make dinner.

user21820

09:36

Sure. No problem.

Let me however finish what I was going to say because it may be relevant in the future. If your MS is a good enough set theory, then you very well can quantify over all these things as I just did: ∀S ( S is a structure ⇒ ... ).

But you may not be able to construct a set of all structures... So you cannot say ∀S∈Structures ( ... ).

This is a limitation of almost any foundational system, so don't assume that every notion in logic is captured by a set. Most are not.

user400188

I must confess that I do not know a lot about set theory. It was a long term goal to learn the specifics when they became necessary for my learning in logic. I can see that they would be helpful now, but I would prefer to finish my current online course and related ones before delving too deeply into it. They are meant to be self contained. Maybe they will cover some of it, or maybe they will just mention the relevant aspects.)

In any case, could you address the 2nd comment I brought up? Namely that I didn't prove that $\exists x (x=a)$ is a valid statement by assuming that its negation was true in all interpretations and deriving a contradiction, but by assuming that it was true in some interpretations and deriving a contradiction. They would prove very different things, and I think it is a small mistake in your answer.

user21820

@user400188 You may not need to know set theory now, but at least you have to understand that a rigorous proof in MS about logic still needs to be one that you can write like this. If you are unable to write out a Fitch-style proof that only uses definitions or axioms or previous theorems of MS, then you simply do not have a rigorous proof.

user400188

I'm currently working on a type up of something like it.

user21820

@user400188 True in every interpretation is equivalent to its negation is false in every interpretation. So the current version of my answer (after Noah pointed out my careless errors) is correct.

Whether you wrap it up as a contradiction proof does not matter at all as the core is unchanged (and unjustified in your post).

user400188

Sorry, you're right. I should have noticed that sooner.

user21820

09:50

@user400188 When you've written it up, feel free to post it here and we can discuss it.

user400188

I'm about to post it, however its not completely symbolic yet. I think it's worth putting here though.

Take any FOL interpretation that interprets $a$ as a variable or constant.

> Assume that $\exists x(x=a)$ is invalid.

> > Then, in some interpretation $I$, $I\vDash\lnot\exists x(x=a)$, and hence $I\vDash\forall x\lnot(x=a)$.

user21820

Type it up in a separate text editor and then paste the whole lot at one go.

Then click the option for "fixed font" to preserve spacing. (This button only appears if your text has more than one line.)

user400188

Oh, I thought you needed posts to indent properly. Thanks.

Take any FOL interpretation that interprets $a$ as a variable or constant.
  Assume that $\exists x(x=a)$ is invalid.
    Then, in some interpretation $I$, $I\vDash\lnot\exists x(x=a)$, and hence $I\vDash\forall x\lnot(x=a)$.
    If we instance x to a with $I[x:=a]\vDash\forall x\lnot(x=a)[x:=a]$ we get $I\vDash\lnot(a=a)$
    This is a contradiction.
  So it must be the case that $\exists x(x=a)$ is valid.

Ah, not rendering Mathjax.

user21820

Yea fixed font is for code, so no formatting except indentation works.

@user400188 So the problem in your 'proof' is what I pointed out at the beginning; you did not prove ( $I\vDash\lnot\exists x(x=a)$ implies $I\vDash\forall x\lnot(x=a)$ ).

1 hour ago, by user21820

@user400188 By the way, what I am saying is that you did not prove the implicit claim ( "∃x ( x=a )" is invalid implies "∀x ( ¬(x=a) )" is true in some interpretation ). That is why it is not rigorous. In contrast, there are no missing steps in my answer, given appropriate definition of FOL tautology.

It's true that now you added one step in-between your original steps in your post, but the main gap is still there.

user400188

yes, I am still not sure how to approach that other than to do a full FOL proof.

user21820

09:59

@user400188 And that is precisely the problem! That is a syntactic way, not semantic.

The semantic way is via what I did in my post, by definition of the semantics of "∃".

For a syntactic way to work, you would have to rely on a theorem that FOL deduction is sound for FOL semantics, and to prove this theorem needs precisely the same thing missing from your proof.

So...

There's no way around it.

user400188

I honestly don't know the semantic way to go from $I\vDash \lnot \exists x(Ax)$ into $I\vDash \forall x\lnot (Ax)$. It seems as natural to me as your step from I[x:=a^I] ⊨ x=a to I ⊨ ∃x ( x=a ).

user21820

@user400188 You're wrong then. As I said, I'm only using the definition of FOL semantics, whereas you're using unproven claims.

user400188

Do I just use I[x:=s]⊨ As, and then quantify over it like you would in a deductive system where $\lnot\exists x(Ax)$ can be used like a universal quantifier?

Part of the problem may be that I have seen so many deductive systems now that one way of doing things doesn't seem any more natural or unproven than another. They all end up proving the same things, and verify each other, so what does it matter?

user21820

@user400188 I don't know what you're trying to do now. You wrote "I[x:=s]⊨ As" but I really have no idea why. Why don't you explicitly write down the definition of "∃" in FOL semantics? If you cannot then you cannot prove anything about FOL.

@user400188 The point is that you haven't proven that! You are claiming something about FOL structures, with no justification at all. This is not a matter of different choice of MS. This is a matter of you not having given any proof in any MS.

@user400188: Before we go on, I really want to see your definition of FOL semantics. Please write it down here without referring to any material or notes.

user400188

The thing is, how did you go from I[x:=a^I] ⊨ x=a to I ⊨ ∃x ( x=a )? Is it taken as primitive in the meta system? If so, why can't I⊨¬∃x(Ax) into I⊨∀x¬(Ax) as well? (Perhaps in some other meta system.)

@user21820 sure

user21820

10:12

@user400188 It's not primitive; it's by the standard definition of FOL semantics.

That's why we cannot go on until you write down your definition.

user400188

I will be referring to predicate logic under Tarskian semantics, which is the traditional semantics for predicate logic. It is based on the notion of interpretations of names in terms of objects external to the logic.

**Objects:** These are the things you are currently talking about. They can be abstract mathematical objects, or objects in the real world.

**Names:** These are the names given to objects. When I refer to a cat, I do not staple the cat to paper as part of my sentence, I use a name. This same distinction between names and objects is made in predicate logic.

user21820

Sorry, that is not a definition of FOL semantics.

(And to address the implicit inquiry, no, we cannot just arbitrarily choose a meta-system that assumes whatever we like, otherwise we are not actually proving anything.)

user400188

I didn't mean to say that an arbitrary one will do. But if we could show that one works, and it works iff another one does, then it should be safe to use the other instead if we like.

user21820

(You cannot show that a meta-system with your kind of assumptions is as safe as mine without doing much more than the work that I did in the post.)

You really need to get a proper textbook. If you have strong mathematical background outside logic, you can consider Rautenberg. If not, maybe try Hannes' notes.

user400188

That is as close to a definition that I have. If it's not what you want, then I'm afraid I can't answer.

I have interpreted FOL semantics to mean the underlying structure behind the FOL proofs we do in deductive systems.

user21820

10:19

Because right now you have not at all defined FOL semantics.

I can give you a proper definition here if you like, but maybe try one of the suggested material first.

It's not at all what you think.

(And now I understand why you think your reasoning is as natural as mine, because you are basically using your external reasoning to talk about the reasoning inside FOL, which is not at all what we need to do to prove the desired stuff.)

user400188

@user21820 Yes, that is what I had assumed "semantics of FOL" meant.

user21820

Yes and now I understand where your misconceptions are coming from. As I said, if you like I can give you a proper definition of FOL semantics here, as an interim measure before you actually read a proper logic text.

Let me know what you prefer. Some people prefer to read it on their own from standard logic texts, but other people prefer my way of doing things.

user400188

I'm currently watching an online course "Advanced Logic (Kurt Gödel’s Greatest Hits)" and have also completed the Stanford Intro to Logic course. The level of the material is undergraduate and high school, respectively.

I prefer the self contained way of a standard logical text, but I have found about 1/3 of your explanations helpful in the past (and all of the discussions with you).

So, if you were to mention a text, then I probably wouldn't get around to it in the near future, as I need to finish the current course. For this reason the definition in chat is the best option (I think).

user21820

Ok.

Let's start from scratch. We are working in MS and want to define FOL. We have an alphabet (you can think of it as ascii for now), and we can reason about finite strings (from said alphabet). I'll leave the details of defining well-formed formulae to you, but suffice to say we can write a program that on any given input string will answer whether or not it is well-formed. For convenience, we allow multi-char names for variables and constant/function/predicate-symbols.

(By leaving it to you I don't mean it is trivial; you will need to do a proper recursive construction, but since I will do one for semantics you can see how it is done and learn to do the same.)

(In MS) we have some basic set theory, and of course we can make definitions. In particular we will write "We say A is an apple iff (A is such that) ..." (with the defined symbol bolded to make the intent clear), meaning that we add the predicate symbol "apple" (in MS!) and the axiom "∀A ( apple(A) ⇔ ... )".

For convenience, let us require that names for variables are distinct from names for non-logical symbols (constant/predicate/function-symbols). We say that L is an FOL language iff L = ⟨C,F,P⟩ where C is a set of strings and F is a set of pairs ⟨f,k⟩ where f is a string and k∈ℕ, and P is a set of pairs ⟨Q,k⟩ where Q is a string and k∈ℕ. C,F,P represent constant-symbols, function-symbols, and predicate-symbols, respectively. The attached natural number represents the number of inputs.

We say that M is an FOL structure over L iff L is an FOL language ⟨C,F,P⟩ and M = ⟨D,IC,IF,IP⟩ where D is a non-empty set and:

(1) IC : C→D.
(2) IF is a function on F such that IF(⟨f,k⟩) ∈ (D^k→D) for every ⟨f,k⟩∈F.
(3) IP is a function on P such that IP(⟨Q,k⟩) ∈ (D^k→Bool) for every ⟨Q,k⟩∈P.

Given FOL structure M = ⟨D,IC,IF,IP⟩, we define dom(M) = D. (Again, this is a kind of definition we can make in MS).

We say that V is a variable assignment over M iff M is an FOL structure V is a function that maps every variable to a member of dom(M).

@user400188: So far okay? These are the necessary stuff we need to set up before we can even start to define FOL semantics.

Note that in the above definition "FOL structure" is a 2-input relation. We can reuse the term to define a 1-input relation: We say that M is an FOL structure iff there is some L such that M is an FOL structure over L.

Note also that given any FOL structure M = ⟨D,IC,IF,IP⟩, we can define lang(M) = ⟨dom(IC),dom(IF),dom(IP)⟩ (here "dom" means just the usual function domain), and then we would be able to prove that M is an FOL structure over lang(M). Informally, this shows that an FOL structure already specifies its own language.

user400188

11:01

Are IF and IP and IC supposed to represent interpretations of functions, predicates, and constants respectively?

user21820

@user400188 Right! Sorry I didn't say it; I wanted to but forgot after listing them out.

user400188

Why is a variable assignment necessary, but not a constant assignment?

user21820

@user400188 Constants are interpreted by IC. Variables need to be handled separately, because they behave differently from constants.

And an FOL structure has no variables!

user400188

Right, i just don't see the reason yet for us not to write M = ⟨VD,IC,IF,IP⟩ , instead of M = ⟨D,IC,IF,IP⟩.

user21820

@user400188 Do you mean "...V,D..."? If not I cannot make sense of "VD".

And I missed out one word above:

> We say that V is a variable assignment over M iff M is an FOL structure and V is a function that maps every variable to a member of dom(M).

user400188

11:09

Oh, well we have an interpretation which maps parts of the domain to functions, why not have a similar thing for variable assignments?

user21820

@user400188 I have no idea what you are talking about. There is no mapping of parts of any domain to functions.

user400188

Sorry, I must have misunderstood IF(⟨f,k⟩) ∈ (D^k→D) for every ⟨f,k⟩∈F. What does it mean for an interpretation to be in (D^k→D)?

user21820

@user400188 (D^k→D) is the collection of functions from D^k to D. Aren't you familiar with this standard mathematical notation?

In more English, IF(⟨f,k⟩) is a function from D^k to D.

user400188

I'm not in the field of mathematics, so a lot of this is foreign to me. I can sort of get the meaning from a lot of it, but I am not aware of the standards.

user21820

@user400188 Ok then please let me know because I had assumed you were an undergraduate mathematics major. (Obviously a bad assumption on my part.)

user400188

11:15

Oh, nothing of the sort. I'm in a PHD for experimental physics at the moment, and did an undergraduate in Robotics and Physics.

user21820

When we write "f : S→T" it means the same as "f ∈ (S→T)" which ties in with the underlying set theory where we can define "S→T" to denote the collection of functions from S to T.

Does it make sense now?

user400188

I think so.

user21820

Ok good.

Now on to FOL semantics.

user21820

11:32

We say that I is an FOL interpretation over L iff I = ⟨M,V⟩ where M is an FOL structure over L and V is a variable assignment over M.

Given any FOL interpretation I = ⟨M,V⟩ over L, and any c ∈ dom(M), and any variable v, we define I[v:=c] = ⟨M,V'⟩ where V' = ( var w ↦ w = v ? c : V(w) ).

This last bit means that V' is a function that on input variable w will output c if w = v but otherwise output V(w).

Informally, I[v:=c] is the same as I except that the variable assignment is overridden for variable v, mapping it to c instead.

Given any FOL interpretation I = ⟨M,V⟩ over L, we recursively define ⊨ as a binary relation such that:

(1) ( I ⊨ "¬"+A ) iff ( I ⊭ A ), for any formula A.
(2) ( I ⊨ A+"∧"+B ) iff ( I ⊨ A ) and ( I ⊨ B ), for any formulae A,B.
(3) ( I ⊨ A+"∨"+B ) iff ( I ⊨ A ) or ( I ⊨ B ), for any formulae A,B.
(4) ( I ⊨ A+"⇒"+B ) iff ( ( I ⊨ A ) implies ( I ⊨ B ) ), for any formulae A,B.
(5) ( I ⊨ "∀"+v+"("+A+")" ) iff ( ( I[v:=c] ⊨ A ) for every c ∈ dom(M) ), for any formula A and variable v.
(6) ( I ⊨ "∃"+v+"("+A+")" ) iff ( ( I[v:=c] ⊨ A ) for some c ∈ dom(M) ), for any formula A and variable v.

Now you have the full definition.

@user400188: Do you understand FOL semantics now?

user400188

Can't say I do, because I haven't finished reading it all yet. But I think it will take a long time to understand all of this even if I do.

user21820

Oh wait, one last bit. I've defined what "⊨" means for interpretations. We still need to go back to structures, because that is the main thing in FOL. Interpretations are almost totally forgotten once we have set up FOL and finished the completeness theorems.

user400188

I can at least see how the variable assignment is kept seperate from everything else, and how an interpretation is a variable assignment and a structure.

user21820

Given any FOL structure M over L and a sentence Q over L (as I said, I haven't defined well-formed formulae over a language, but you can try it out!), we say that M ⊨ Q iff ( ⟨M,V⟩ ⊨ Q for every variable assignment V over M ).

Tada we are done.

Oh wait I completely forgot in defining "⊨" to define for interpreting symbols lol!

Give me a while to add those in.

user400188

11:49

@user21820 These definitions to me look similar to those for FOL theories. (1) consistent, (2) something, (3) prime, (4) something, (5) universal, (6) witnessed.

user21820

I have no idea what "something" or "prime" you are talking about.

user400188

Oh, something was what I used when I didn't know the name of the property.

user21820

We recursively define ⊨ and eval such that for any FOL interpretation I = ⟨M,V⟩ over L = ⟨C,F,P⟩ where M = ⟨D,IC,IF,IP⟩:

(1) ( I ⊨ "¬"+A ) iff ( I ⊭ A ), for any formula A over L.
(2) ( I ⊨ "("+A+"∧"+B+")" ) iff ( I ⊨ A ) and ( I ⊨ B ), for any formulae A,B over L.
(3) ( I ⊨ "("+A+"∨"+B+")" ) iff ( I ⊨ A ) or ( I ⊨ B ), for any formulae A,B over L.
(4) ( I ⊨ "("+A+"⇒"+B+")" ) iff ( ( I ⊨ A ) implies ( I ⊨ B ) ), for any formulae A,B over L.
(5) ( I ⊨ "∀"+v+"("+A+")" ) iff ( ( I[v:=c] ⊨ A ) for every c ∈ D ), for any formula A over L and variable v.
(6) ( I ⊨ "∃"+v+"("+A+")" ) iff ( ( I[v:=c] ⊨ A ) for some c ∈ D ), for any formula A over L and variable v.

Ok here is the full definition. I think I didn't miss anything now.

user400188

Prime is a definition I encountered in the logic course. If $A\lor B\in T$ iff either $A\in T$ or $B\in T$, then T is said to be prime. It is useful to notice that a FOL theory is prime, as any prime theory is complete.

user21820

I changed the phrasing a bit, because we cannot define ⊨ just for one I. And we have to define eval at the same time or before ⊨. And I added "over L" at all relevant places so that we don't have rubbish when the formula is not over the language of the interpretation.

Anyway the whole point of this is to define FOL semantics. Without such a recursive definition, we simply cannot reason rigorously about FOL at all.

Ok I need to go soon. But just to complete the discussion, in my post I was using "M[x:=a^M]" to mean the interpretation ⟨M,V⟩ where V maps "x" to a^M and every other variable to some arbitrary thing (it does not matter). We could alternatively allow a variable assignment to not map all variables, but for simplicity I did not do it in the above chat discussion.

Note that by definition (point 6) ( M["x":=a^M] ⊨ "x=a" ) implies ( M ⊨ "∃x ( x=a )" ) as desired.

user400188

12:01

It is getting late where I am too, and I'm sure you have spent more time than you originally intended to helping me.

Thank you for all the help with the answer I provided and the answer to my question. As well as the definitions of semantics of FOL, and my misconceptions of them. It is sincerely appreciated.

user21820

@user400188 You're welcome! Let me know next time if you have any further inquiries.

user400188

I feel like I should accept your answer over mine in the meantime in that post. I'm unlikely to edit it so its a rigorous proof that ∃𝑥(𝑥=𝑎) is a valid formula without copying one of your examples. Hopefully though, I can construct such a proof sometime in the future.

user21820

@user400188 Of course I would prefer if you accept my answer, but that's your choice. In any case, I applaud you for wanting to take an unclear question and make it clear and also address the inquiry. If you didn't try it we wouldn't have been able to have this great discussion. =)

I didn't ever write it out completely like I did here because I was always too lazy and just pointed people to Hannes's notes hahaha..

His version of this thing is in Section 3 under Definition 7.

Same ingredients, just different presentation.

Oh oops on looking at Hannes' version, I see I missed one final case:

(11) eval( v ) = V(v), for any variable v.

user21820

12:25

Let's put the whole thing in one place for anyone who wants to refer to it:

We are working in MS (meta-system) and want to define FOL. We have an alphabet (you can think of it as ascii for now), and we can reason about finite strings (from said alphabet). In MS we have some basic set theory, and of course we can make definitions. In particular we will write "We say A is an **apple** iff (A is such that) ..." (with the defined symbol bolded to make the intent clear), meaning that we add the predicate symbol "apple" (in MS!) and the axiom "∀A ( apple(A) ⇔ ... )". See [this](https://math.stackexchange.com/a/1864310/21820) for details on how we can make definitions).

@JackOhara: You may want to read it as I recall we had some discussions about FOL semantics before as well.

user21820

12:38

Hmm.. I keep forgetting that formatting does not work in multiline text. So annoying.

user21820

19:28

→ 5 messages moved to Basic Mathematics

Transcript for

♦ $Mathematics$ Logic

Transcript for

♦ Logic

♦ $Mathematics$ Logic