0

My understanding of QPL so far is that we can quantify over propositions so as to say things like, "There is a proposition such that..." or at least, "There is an x such that x is a proposition and..." My initial use of this kind of sentence was in the form of, "There is an axiom such that..." Question: would it be more "proper" to say, "There is a proposition such that it is axiomatic," here, or can we bring in many-sorted logic and divide axioms and theorems into at least two of the sorts of an MSQPL?

Kristian Berry
  • 9,561
  • 1
  • 12
  • 33
  • It feels to say "there is an axiom such that...", maybe. Isn't it redundant with just stating the axiom itself directly? – Frank Jan 01 '23 at 00:11
  • 1
    @Frank, the redundancy issue is of a piece with the ["paradox" of foundationalism](https://philosophy.stackexchange.com/questions/82457/a-paradox-of-foundationalism). See Adam Sharpe's answer for reasons to think that evaluating axioms with reference to other propositions is not an ill-formed notion. My motivation for exploring this territory currently is in trying to formalize a version of set theory based on an "axiom scheme of excession," which is based on the idea that some/many axioms are "exceeded" as we ascend the cumulative hierarchy. – Kristian Berry Jan 01 '23 at 00:47
  • 1
    This also turned into an attempt to characterize a genus of large cardinals based on *how* excessive their axioms are: the hypothesis scheme is, "There is an axiom such that it takes *n* steps to overgeneralize from that axiom, another that it takes *m* steps to overgeneralize from, and if *n* < *m*, the cardinal for the *n*-axiom is *larger* than the cardinal for the *m*-axiom." – Kristian Berry Jan 01 '23 at 00:50

1 Answers1

1

It is commonplace in natural language to quantify over propositions. E.g. "The witnesses contradict each other, so at least one of their statements is false", "everything Smith said in his speech is nonsense", "whatever the Pope says is true".

A proposition can be thought of as a zero place predicate. So, if you are quantifying over propositions you are using second order logic, or at least a fragment of it. If you restrict the quantification to zero place predicates only, and you have no additional functions or operators on propositions, including identity between propositions, then you can map this into first order logic. But that is not very useful: it does not allow you to say anything about propositions, which is presumably why you wanted to quantify over them in the first place.

If you want to be able to say that it is a property of some proposition that it is an axiom, i.e. (∃p)Axiom(p) then you will need some additional axioms or rules within the logic to express how to quantify into a propositional position. There are some systems that have been devised for this purpose, e.g. that of Arthur Prior. It doesn't matter much whether you prefer to treat 'axiom' as a type or as a property.

Bear in mind that quantifying over propositions can lead to semantic paradoxes, especially if you include a truth predicate. "Everything I say is false" leads to a version of the liar paradox.

Bumble
  • 20,757
  • 2
  • 27
  • 65
  • I do have a curious motive for wanting to identify axioms and theorems as different sorts, here, but I'm going to wait until I decide whether to ask about my "axiom scheme of excession" to go over the details. That post will itself have to wait until I can figure out how to frame it without making it into a "personal theory" post. – Kristian Berry Jan 01 '23 at 05:04