I have a doubt about open formulas in first order logic. Every time i define an open formula i put terms inside it. For example i can have $Q(x)$ as an open formula.
Is the term $x$ intended as a constant (ground term) ?
I have a doubt about open formulas in first order logic. Every time i define an open formula i put terms inside it. For example i can have $Q(x)$ as an open formula.
Is the term $x$ intended as a constant (ground term) ?
Copyright © 2021 JogjaFile Inc.
From a syntactic point of view the difference between a constant and a variable is that you can quantify over a variable but you cannot quantify over a constant.
From a semantic point of view a structure has to provide an interpretation for constants but not for variables.
The intuition is that variables represents generic elements of the semantic domain, that is they represent elements of the semantic domain that can be substituted by any other element of the domain.
Constants in the other hand represent fixed elements of the domain, elements that should be not replaced by any other element.
Edit: As pointed out in the comments a variable can be considered just as a generic constant, that is a constant over which we don't make any assumption. This means that, by convention, we are not allowed to use axioms containing free variables in theories.
This choice has two consequences:
From a syntactical point of view, since we are not making any assumption on variables, we have that in any valid proof (i.e. a tree of formulas build according to some inference rules) if we replace all the occurrences of a given variable with a term we still get a valid proof (this can be proved by induction on the proofs). This basically means that everything that can be proven for a variable can be proven for any other object, which is what we really need variables for.
From a semantic point of view, since variables are not allowed to appear free in axioms of a theory we don't need to provide an interpretation for them in a structure: since they don't occur in axioms, assigning to them different values wouldn't change whether the axioms are true or not in the structure, so it is meaningless assigning values to them.
Hope this helps.