Finitization rule

https://mathoverflow.net/questions/349084/at-which-large-cardinal-property-ackermann-this-finitization-rule-would-fail

An nn-ary meta-theoretic variable with respect to language LL is an expression of the form ϕ(x1,..,xn)ϕ(x1,..,xn) that is meant to range over all formulas of LL that have all symbols x1,..,xnx1,..,xn as their sole free variables.

Let QLQL be a schematic expression, taken to mean a string of symbols in which there occur nn-ary meta-theoretic variable symbol(s) such that if all those meta-theoretic variables are substituted by formulas of language LL they range over, then the result would be a formula of language LL.

Lets denote ‘‘QL≡"‘‘QL≡" to signify the schema of all sentences in language LL that result from all substitutions of all the meta-theoretic variables occurring in QLQL.

An example of such a schematic expression is the expression "x∈A∧ϕ(x)x∈A∧ϕ(x)", here ϕ(x)ϕ(x) is the meta-theoretic variable symbol that range over all formulas of the language of set theory in which the symbol xx occur free. Now "[x∈A∧ϕ(x)]≡[x∈A∧ϕ(x)]≡" is the schema of all formulas in the language of set theory that results from all substitutions of the meta-theoretic variable ϕ(x)ϕ(x) by the formulas it range over.

Now what I want to investigate here are ways to finitely express the whole schema QL≡QL≡ in some language L+L+ that extends LL

Now by finQL,L+finQL,L+ it is meant a single formula in language L+L+, that results from replacing all meta-theoretic variables of the schematic expression QLQL into special kind of classes that are expressible in language L+L+, like through taking the following steps:

Each nn-ary [n>0] meta-theoretic variable ϕ(x1,..,xn)ϕ(x1,..,xn) is replaced by ⟨x1,..,xn⟩∈P⟨x1,..,xn⟩∈P for n>1n>1, Where ⟨ 1,.., n⟩⟨ 1,.., n⟩ signify an n-ary tuple. For the case where n=1n=1, then ϕ(x1)ϕ(x1) would be replaced by x1∈Px1∈P. The whole expression is preceded by the string of all class symbols replacing the meta-theoretic variable symbols, according to the order of their first appearance in the schematic expression QQ and all of them are universally quantified.

Example: the schema

[∀x1∈V∃x∈V∀y∈V(y∈x↔y∈x1∧ϕ(y))]≡[∀x1∈V∃x∈V∀y∈V(y∈x↔y∈x1∧ϕ(y))]≡,

where ϕϕ is bounded by VV formula that doesn't use VV otherwise.

Would turn into the single sentence:

∀P[∀x1∈V∃x∈V∀y∈V(y∈x↔y∈x1∧y∈P)]∀P[∀x1∈V∃x∈V∀y∈V(y∈x↔y∈x1∧y∈P)]

Another example: the replacement schema of Ackermanns,

[∀A∈V∃B∈V∀y∈V(y∈B↔∃x∈V(x∈A∧∀z∈V(ϕ(x,z)↔z=y)))]≡[∀A∈V∃B∈V∀y∈V(y∈B↔∃x∈V(x∈A∧∀z∈V(ϕ(x,z)↔z=y)))]≡

where ϕϕ is bounded by VV formula that doesn't use VV otherwise.

This would turn into the single sentence:

∀P[∀A∈V∃B∈V∀y∈V(y∈B↔∃x∈V(x∈A∧∀z∈V(⟨x,z⟩∈P↔z=y)))]∀P[∀A∈V∃B∈V∀y∈V(y∈B↔∃x∈V(x∈A∧∀z∈V(⟨x,z⟩∈P↔z=y)))]

What we want to motivate here is the ability to have following infinite inference rule (under certain specifications):

QL≡−−−−finQL,L+QL≡−−−−finQL,L+

The idea is to have the following reflective class theory defined in the first order language of set theory plus an additional primitive constant symbol VV, so we have L=FOL(=,∈,V)L=FOL(=,∈,V) with axioms:

Extensionality: ∀Z(Z∈X↔Z∈Y)→X=Y∀Z(Z∈X↔Z∈Y)→X=Y

Transitivity: X∈Y∈V→X∈VX∈Y∈V→X∈V

Class construction schema: if ϕϕis a formula in which the variable symbol xx doesn't occur free; then all closures of:

; are axioms.

Reflection schema: if ϕϕ is a formula in which all and only symbols X,X1,..,XnX,X1,..,Xn occur free; and only free; that doesn't use the symbol VV, then:

, is an axiom.

Foundation: ∃X(X∈Y)→∃X∈Y∀Z∈Y(Z∉X)∃X(X∈Y)→∃X∈Y∀Z∈Y(Z∉X)

Finitization inference rule:

[∀x1∈V,..,∀xn∈V∃x∈V∀y∈V(y∈x↔QLset)]≡_______________________________________∀P1,..,∀Pm[∀x1∈V,..,∀xn∈V∃x∈V∀y∈V(y∈x↔finQLset,L)][∀x1∈V,..,∀xn∈V∃x∈V∀y∈V(y∈x↔QLset)]≡_______________________________________∀P1,..,∀Pm[∀x1∈V,..,∀xn∈V∃x∈V∀y∈V(y∈x↔finQLset,L)]

where mm is the total number of metatheoretic varaibles in QQ

Where LsetLset is the Ackermannian language of set theory, i.e. the set of all formulae that results from bounding all quantifiers in pure set theoretic formulas (i.e.; FOL(=,∈)FOL(=,∈)) by the symbol VV, whose free variables are all and only symbols y,x1,..,xny,x1,..,xn.

Now the finitization rule would result in proving that VV is super-transitive! Also it would prove that every set sized subclass of VV is a set, thereby pumping up VV to a near Mahlo in cardinality! I wonder if the finitization rule can work to prove that VV is a Mahlo? Or whether it can even go beyond this?

Question 1: what is the smallest large cardinal this theory cannot construct?

The above finitization rule was a caustious variant. However the more general original variant was:

QLset≡−−−−−finQLset,LQLset≡−−−−−finQLset,L

Question 2: is there a clear inconsistency with this general finitization rule?