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.
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.