new preprint about an interesting new approach to logic

[CRGreathouse]

Therefore #1 would be a member of its image, and as far as I know, no function is a member of its image.

I don't see why not, and Peter Aczel didn't either.

Is such a function prohibited by your logic? I saw no such prohibition.

Regardless, I don't see where your assumption that the S2 proof uses # comes from, nor why #2(ε,#,ε) = #1.

[avonm]

using the axiom of regularity you can prove that
- no set is a member of itself (wikipedia)
- no function is a member of its domain
- no binary relation is a member of its domain.

In a similar way you should be able to prove that no function is a member of its image.

Regardless, I don't see where your assumption that the S2 proof uses # comes from, nor why #2(ε,#,ε) = #1.

The symbol # appears at least 7 or 8 times in that proof. And it's quite obvious that #2(ε,#,ε) = #1, because when we use the symbol # its meaning is precisely #1.

[CRGreathouse]

using the axiom of regularity you can prove that
- no set is a member of itself (wikipedia)
- no function is a member of its domain
- no binary relation is a member of its domain.

The axiom of regularity is a part of ZF, but I didn't see it in your logic. And that would be a very unusual thing for a logic to have; Enderton's first-order logic doesn't include it, and I don't know of any logic that does. There are set theories with it and without it (Aczel has some of the most famous of the "without").

And it's quite obvious that #2(ε,#,ε) = #1, because when we use the symbol # its meaning is precisely #1.

Since you never actually defined # that's not obvious to me. You just gave a vague description.

[avonm]

I didn't see it in your logic

The reasoning was not a reasoning in 'my logic' it was simply a reasoning to prove that the proof of consistency of S1 cannot be internal to s1.
As far as I know if you don't accept the axiom of regularity you fall into rather counterintuitive theories where a function can be a member of its domain, a set can be a member of itself and so on.

In any way, it seems clear that the proof of consistency is external to S1 so using goedel second incompleteness theorem by contraposition it follows that the consistence cannot be proved internally in S1.

Since you never actually defined # that's not obvious to me. You just gave a vague description.

Definition 2.1 begins on page 9 and ends on page 51, it fully defines # .

[CRGreathouse]

The reasoning was not a reasoning in 'my logic' it was simply a reasoning to prove that the proof of consistency of S1 cannot be internal to s1.

So if the regularity axiom isn't a part of your logic you can't assume it, because there are (presumably) models of your logic which are not well-founded. (Probably the only way that such models can fail to exist is if your system is inconsistent.)

As far as I know if you don't accept the axiom of regularity you fall into rather counterintuitive theories where a function can be a member of its domain, a set can be a member of itself and so on.

I should mention that I don't accept the axiom of regularity myself*, so I see nothing wrong with this.

* I like ZF \ Regularity, so I accept the LEM and Axiom of Infinity but reject AC and Regularity.

Definition 2.1 begins on page 9 and ends on page 51, it fully defines # .

Hmm, I guess that's why I missed it, it's hard to remember that you're inside a definition the whole time!

I'll be honest -- I can't justify the time it would take to carefully parse this 42-page definition. I wish you luck finding people to look over your work.

[avonm]

So if the regularity axiom isn't a part of your logic you can't assume it

The proof of consistency is external to the system instance, this holds independently from regularity, and consistency of any instance is shown independently from regularity. Regularity was just used to further document the fact that the same proof cannot become an internal proof, but this also holds by using goedel second incompleteness theorem by contraposition.
There are models (i.e. instances) of my system that don't use regularity, and they are consistent because all models are consistent.

I consider the topic about consistency is clarified. I'll probably not repost about this, since I don't see any consistency issue about my system.

As a further reference on this topic i can cite this part of wikipedia's article about goedel's incompleteness theorems.

The second incompleteness theorem only shows that the consistency of certain theories cannot be proved from the axioms of those theories themselves. It does not show that the consistency cannot be proved from other (consistent) axioms. For example, the consistency of the Peano arithmetic can be proved in Zermelo–Fraenkel set theory (ZFC), or in theories of arithmetic augmented with transfinite induction, as in Gentzen's consistency proof.