= 27d567bc2d48d9f40e9ccc20ea370b15)
Eugine_Nier comments on Logical Pinpointing - Less Wrong
You are viewing a comment permalink. View the original post to see all comments and the full post content.
= 783df68a0f980790206b9ea87794c5b6)
Loading…= b715d02e85f7b3b4ae65ca3d3e450868)
Subscribe to RSS Feed
Powered by Reddit
= f037147d6e6c911a85753b9abdedda8d)
You are viewing a comment permalink. View the original post to see all comments and the full post content.
Comments (338)
If you're already fine with the alternating quantifiers of first-order logic, I don't see why allowing branching quantifiers would cause a problem. I could describe second order logic in terms of branching quantifiers.
Huh. That's interesting. Are you saying that you can actually pin down The Natural Numbers exactly using some "first order logic with branching quantifiers"? If so, I would be interested in seeing it.
Sure:
It is not the case that: there exists a z such that for every x and x’, there exists a y depending only on x and a y’ depending only on x’ such that Q(x,x’,y,y’,z) is true
where Q(x,x’,y,y’,z) is ((x=x' ) → (y=y' )) ∧ ((Sx=x' ) → (y=y' )) ∧ ((x=0) → (y=0)) ∧ ((x=z) → (y=1))
Cool. I agree that this is potentially less problematic than the second order logic approach. But it does still manage to encode the idea of a function in it implicitly when it talks about "y depending only on x", it essentially requires that y is a function of x, and if it's unclear exactly which functions are allowed, you will have problems. I guess first order logic has this problem to some degree, but with alternating quantifiers, the functions that you might need to define seem closer to the type that should necessarily exist.