2

I came across two axioms involving the satisfaction predicate (in sequent calculus),

(SatI) P(z1, z2, ..., zn) ⊢ Satn(z1, z2, ..., zn, ⌜P(x1, x2, ..., xn)⌝)
(SatE) Satn(z1, z2, ..., zn, ⌜P(x1, x2, ..., xn)⌝) ⊢ P(z1, z2, ..., zn)

Where P is an n-ary predicate, Satn is an (n+1)-ary Satisfaction predicate, and the quote ⌜⌝ is some formula naming device (i.e. Godel code).

I'm wondering if the following modified version, which is less restrictive, is problematic:

(SatI') Φ [z1/x1][z2/x2]...[zn/xn] ⊢ Satn'(z1, z2, ..., zn, ⌜Φ⌝)
(SatE') Satn'(z1, z2, ..., zn, ⌜Φ⌝) ⊢ Φ [z1/x1][z2/x2]...[zn/xn]

Here, Φ[z1/x1][z2/x2]...[zn/xn] is Φ with each occurence of x1 replaced by z1, x2 replaced by z2, etc. Defining the Satisfaction predicate this way allows me to treat formulas with free variables as "predicates," instead of restricting formulas the Satn can take to be some predicate P. For example, I can define the Heterological predicate as:

H(z) ≡ ¬Satn'(z, ⌜x1(x1)⌝)

Sorry for the hard-to-read notation, afaik it doesn't allow latex rendered stuff here

ayylien
  • 129
  • 8
  • Though you aim to broaden the existing satn intro/elim axioms to include formulas with free variables, however, Gödel encoding only makes sense in PA like formal system, thus the existing predicate P can hardly be about those which are not already formulas with free variables as shown in P’s arguments… – Double Knot Mar 06 '24 at 07:54
  • @DoubleKnot I'm not necessarily working in PA (although I could be). As long as there's some formula naming device and the satisfaction predicate is taken to be primitive. You are right though, the formulas whose godel code goes into the original Satn have free variables. The difference between the original axioms and the new one is that under the original axiom, the Heterological predicate must be defined using Sat^2 instead of Sat^1. This affects how the heterological paradox can be proven (I have a specific proof in mind). – ayylien Mar 06 '24 at 21:03
  • Do you mean Sat^2=SatI', Sat^1=SatI above? Note you didn't differentiate the 2 SatE above, do you regard them as exactly same? As for your version expressing heterological predicate simply as H(z) ≡ ¬Satn(z, ⌜x1(x1)⌝) for an arbitrary free variable x1 (do you think it makes sense?), how's your own reference's sequent calculus defines H and do they prove it's a paradox like Russell's using their notation?... – Double Knot Mar 06 '24 at 22:26
  • Sorry for the sloppy notation. I've changed my (SatE) axiom to (SatE') to avoid confusion, and I changed the Satn that I'm using in the new axioms to be Satn' to distinguish from the original Satn. So I'm defining H(z) ≡ ¬Sat^1'(z, ⌜x1(x1)⌝), whereas using the original definition, H(z) would have to be ¬Sat^1(z,z). There's a paper that argued because of the Sat axioms(the old ones with the strict restrictions on arity), the heterological paradox proof needs to utilize the Ref function to make the arities fit. – ayylien Mar 07 '24 at 18:03
  • The ref function basically takes a predicate and reduces its arity by 1. If P takes n+1 arguments, then (Ref P) takes n arguments x0 ... xn where it is equivalent to P(x0, ..., xn, xn). – ayylien Mar 07 '24 at 18:06
  • 1
    So I want to argue against it by changing the Sat axioms in a nonproblematic way, so that the proof of the heterological paradox does not involve Ref. And by doing so, the proof will use the exact same inference rules as another family of paradoxes (which he calls the Unsatisfactory paradox, but it's basically very similar to Heterological or Russell's paradox, except it's about one specific property/set that does not apply to itself/is not a member of itself) His argument is a little complicated, so if you're interested, the paper is Eldridge-Smith (2015), "Two Paradoxes of Satisfaction" – ayylien Mar 07 '24 at 18:07

0 Answers0