Sorry, I used the word “definition” sloppily there. I don’t think we disagree with each other.
I meant something closer to “how equality is formalized in first order logic”. That’s what the bit about the axiom schemas was referencing: it’s how we bake in all the properties we require of the special binary predicate “=”. There’s a big, infinite core of axiom schemas specifying how “=” works that’s retained across FOLs, even as you add/remove character, relation and function symbols to the language.
But I’m pretty sure all instances of the axiom schema
x=y→ϕ(...,x,...)=ϕ(...,y,...)
(for any FOL-definable predicate ϕ in our theory) are already implied if we, as is customary, assume as logic FOL+identity, i.e. first-order predicate logic with a primitive logical predicate for identity. So in that case we don’t need the axiom schema. (And in second and higher order logic we need neither an axiom schema nor a primitive relation, because in that case identity is already definable in pure logic, without any theory, so we have a logical identity relation without having it to add as a primitive.) If we just assume FOL alone, adding this axiom schema to a particular first-order theory makes sense, but I conjecture that it is not equivalent to full (primitive or second-order definable) identity, similar to how the axiom schema of induction is not equivalent to the induction axiom, which requires second-order logic.
I’m confused. In any FOL, you have a bunch of “logical axioms” which come built-in to the language, and axioms for whatever theories you want to investigate in said language. You need these or else you’ve got no way prove basically anything in the language, since your deduction rules are: state an axiom from your logical axioms, from your assumed theory’s axioms, or Modus Ponens. And the logical axioms include a number of axioms schemas, such as the ones for equality that I describe, no?
Yes, with Hilbert proof systems, since those have axioms / axiom schemata. (In natural deduction systems there are only inference rules like Modus ponens, no logical axioms.) But semantically, a “primitive” identity symbol is commonly already interpreted to be the real identity, which would imply the truth of all instances of those axiom schemes. Though syntactically, for the proof system, you indeed still need to handle equality in FOL, either with axioms (Hilbert) or special inference rules (natural deduction).
These syntactical rules are weaker in FOL however than the full (semantic) notion of identity. Because they only infer that all “identical” objects have all first-order definable predicates in common, which doesn’t cover all possible properties, and which holds also for weaker forms of equality (“first-order equivalence”).
Eliezer mentioned the predicate “has finitely many predecessors” as an example of a property that is only second-order definable. So two distinct objects could have all their first-order definable properties in common while not being identical. The first-order theory wouldn’t prove that they are different. The second-order definition of identity, on the other hand, ranges over all properties rather than over all first-order definable ones, so it captures real identity.
Right, if we rely on this notion of “the real identity”. I think discussing that would get into even more confusing territory than just focusing on formalizations that look like they’re some kind of equality.
Sorry, I used the word “definition” sloppily there. I don’t think we disagree with each other.
I meant something closer to “how equality is formalized in first order logic”. That’s what the bit about the axiom schemas was referencing: it’s how we bake in all the properties we require of the special binary predicate “=”. There’s a big, infinite core of axiom schemas specifying how “=” works that’s retained across FOLs, even as you add/remove character, relation and function symbols to the language.
But I’m pretty sure all instances of the axiom schema
x=y→ϕ(...,x,...)=ϕ(...,y,...)
(for any FOL-definable predicate ϕ in our theory) are already implied if we, as is customary, assume as logic FOL+identity, i.e. first-order predicate logic with a primitive logical predicate for identity. So in that case we don’t need the axiom schema. (And in second and higher order logic we need neither an axiom schema nor a primitive relation, because in that case identity is already definable in pure logic, without any theory, so we have a logical identity relation without having it to add as a primitive.) If we just assume FOL alone, adding this axiom schema to a particular first-order theory makes sense, but I conjecture that it is not equivalent to full (primitive or second-order definable) identity, similar to how the axiom schema of induction is not equivalent to the induction axiom, which requires second-order logic.
I’m confused. In any FOL, you have a bunch of “logical axioms” which come built-in to the language, and axioms for whatever theories you want to investigate in said language. You need these or else you’ve got no way prove basically anything in the language, since your deduction rules are: state an axiom from your logical axioms, from your assumed theory’s axioms, or Modus Ponens. And the logical axioms include a number of axioms schemas, such as the ones for equality that I describe, no?
Yes, with Hilbert proof systems, since those have axioms / axiom schemata. (In natural deduction systems there are only inference rules like Modus ponens, no logical axioms.) But semantically, a “primitive” identity symbol is commonly already interpreted to be the real identity, which would imply the truth of all instances of those axiom schemes. Though syntactically, for the proof system, you indeed still need to handle equality in FOL, either with axioms (Hilbert) or special inference rules (natural deduction).
These syntactical rules are weaker in FOL however than the full (semantic) notion of identity. Because they only infer that all “identical” objects have all first-order definable predicates in common, which doesn’t cover all possible properties, and which holds also for weaker forms of equality (“first-order equivalence”).
Eliezer mentioned the predicate “has finitely many predecessors” as an example of a property that is only second-order definable. So two distinct objects could have all their first-order definable properties in common while not being identical. The first-order theory wouldn’t prove that they are different. The second-order definition of identity, on the other hand, ranges over all properties rather than over all first-order definable ones, so it captures real identity.
Right, if we rely on this notion of “the real identity”. I think discussing that would get into even more confusing territory than just focusing on formalizations that look like they’re some kind of equality.