In first order logic, we make quantification over individuals, and in second order logic, we make quantification over properties. So could we supply logics make quantification over logical constants, e.g. over logical connectives, or modalities (intensional logical constants)... I do not have clear image, however, the idea of quantification over logical constants and its property seem of my interest.
Asked
Active
Viewed 60 times
2
-
No; quantifiers apply to "something" that are objects of predication: individuals in first-order, properties of individual in second-order, properties of properties in third, and so on. In all cases, we are speaking of entities of the works. Logical connectives are part of language that we use to build complex statements from simpler ones: in this way, they are not referring to entities. – Mauro ALLEGRANZA Oct 29 '21 at 16:09
-
We can understand e.g. **(∀p)(¬p)** but what does it mean **(∀¬)(¬p)**? – Mauro ALLEGRANZA Oct 29 '21 at 16:16
-
2@MauroALLEGRANZA That won't parse, but something like "(∀*)(*p)" would where * is a "unary connective variable." And the semantics is straightforward (via some pre-set notion of "admissible connectives", or we could bake that into the structure). There's nothing difficult about setting up a logic like this; the real issue is what one would gain in doing so. – Noah Schweber Oct 29 '21 at 16:18
-
1Leśniewski and other Polish logicians included quantification over variables that take truth functions (like connectives) as values in what they called ["protothetic"](https://plato.stanford.edu/entries/lesniewski/#Pro). It is discussed by Church in [Introduction to Mathematical Logic, p. 152ff](https://www.google.com/books/edition/Introduction_to_Mathematical_Logic/JDLQOMKbdScC?hl=en&gbpv=0), who says that it embeds into higher order functional calculi. – Conifold Oct 29 '21 at 17:17
-
First order logics cannot quantify over quantifiers as shown in an example to express "any natural number equals the sum of at most 30 natural numbers." If you have to translate verbatim, then you have to arrive at something like: with one sort Domain=N, ∀n(∃m.0<=m ∧ m<=30 ∧ ∃a1...∃am.(a1+...+am=n)) which is not a wff. You can work around this within FOL by adding disjunctions manually here, if you don't want to use higher order logic to express same. So by using similar tricks FOL only needs to quantify over domain of nonlogical individual symbols to express almost anything. – Double Knot Nov 01 '21 at 20:02