> Am 17.03.2020 um 01:17 schrieb Mario Carneiro <[email protected]>:
>
>
>
> On Mon, Mar 16, 2020 at 4:55 PM Ken Kubota <[email protected]
> <mailto:[email protected]>> wrote:
>
>> Am 16.03.2020 um 23:42 schrieb Norman Megill <[email protected]
>> <mailto:[email protected]>>:
>>
>> On Monday, March 16, 2020 at 1:06:17 PM UTC-4, Ken Kubota wrote:
>> In terms of expressiveness, schemes are another way of expressing what
>> usually requires a higher order.
>> If you want to determine the order of a logic, it doesn't make sense to
>> allow schemes.
>> What can be expressed in first-order logic (FOL) with schemes requires at
>> least second-order logic (without schemes).
>> So it is adequate to state that PA requires second-order logic (i.e.,
>> first-order logic without extensions like schemes is not sufficient).
>>
>>
>> Schemes are used in FOL to describe the axioms. They aren't the axioms
>> themselves.
>>
>> Propositional calculus also uses schemes to describe its axioms. Note that
>> the axioms themselves - an infinite number of them - are not schemes.
>>
>> If the use of schemes in the description of axioms automatically makes a
>> logic second order, then there can be no such thing as first-order logic per
>> your definition, since you can't even specify the underlying propositional
>> calculus without them. Your definition is not the one used in the
>> literature to define first-order logic.
>
> Let me refine my argument by pointing out that the schematic variable
> required for induction in PA in FOL ranges over _predicates_ (unlike the
> schemes in propositional calculus or first-order logic), which renders the
> formal system de facto second-order, since the schema could also be replaced
> by quantification over a predicate variable.
>
> The schematic variable for PA induction does *not* range over predicates, it
> ranges over formulas with one distinguished variable. That is in fact exactly
> what makes the difference between first order and second order formulations:
> in second order PA the induction axiom ranges over all predicates on the
> natural numbers using a second order quantifier. The reason second order PA
> is categorical is because when we interpret the second order quantification
> as a quantification over all subsets, the logic gains access to all
> uncountably many subsets of the natural numbers via this quantifier, while
> first order PA is stuck with talking about only the countably many predicates
> that can be described by a formula.
The formulation that the schematic variable ranges over "formulas with one
distinguished variable" is vague.
The point is that the type of this schematic variable is "oi" (i.e., a
predicate), and not, for example, "o" (proposition). (Clearly, the variable P
in the induction axiom denotes a predicate/property/set.)
Therefore PA cannot be expressed in first-order logic, hence it is at least
second-order.
You seem to follow the semantic approach ("when we interpret").
But from a purely syntactic point of view, the interpretation is not relevant,
but only the fact that all theorems of Peano arithmetic can be obtained
syntactically – given a formal language more expressive than first-order logic.
____________________________________________________
Ken Kubota
doi.org/10.4444/100 <https://doi.org/10.4444/100>
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/F506C23B-814D-4467-8AA3-3ED17FCDD37E%40kenkubota.de.
