BalinKing

> while the other is essentially a definition for anyone who denies that Jesus is Christ, even if their ideological differences are benign?

I don't think this states it strongly enough (sorry for not being clearer originally): In the gospels, Jesus is very black-and-white, e.g. "he who is not with Me is against Me" (Matt. 12:30a). In my reading, the New Testament pretty emphatically denies the existence of "benign" ideological differences, and instead it's a pretty binary you-either-actively-accept-God-or-actively-reject-Him (cf. John 3:16–20 [1], James 4:4 [2], Romans 1:16–32 [3], or Luke 16:19–31 [4]).

Re: your second point about strawmen, I'm a Christian myself and so I suppose I'm gonna have a different take on things :-) Specifically, I think the Bible is true as a matter of fact (e.g. instead of being just a collection of arbitrary books as compiled by the "theological winners" of history [5]). So, I disagree a priori with viewpoints that look at it through a purely political/historical lens. Certainly it's true that the Bible is applicable to politics, and it is a historical document after all, but for me there's not much point in trying to divine the (so to speak) "true motivation" behind it, instead of just taking it at face value. (I'd say something similar about the so-called "historical Jesus", since for me the one presented in the four canonical gospels is the Jesus of history.)

Now, with that said, I do think there's a bit of internal evidence against the idea that the church just wanted to create a vague bogeyman. For one, I think that a literal reading of the relevant passages implies that there is a single (big-A) Antichrist at the end of history. Some Protestants disagree—some denominations consider the Antichrist to be allegorical, while some Lutheran denominations consider the office of the Pope (but not necessarily the person himself) to be the Antichrist—so I'm not claiming that my interpretation is entirely universal, but it is at least fairly common. And so, if there really is only one Antichrist per se, it's harder to apply it to the enemy du jour without looking really silly in hindsight fifty years later (of course, not that this always has stopped people from trying...).

More generally, and here my Protestant bias is showing, I think the Bible warns against the idea of the church being a single earthly institution that gets to set a 100% all-encompassing "party line" for its members: Jesus criticized the Pharisees for making their own arbitrary traditions (Matthew 15:1–7 [7]) and the apostle Paul repeatedly urges Christians to be tolerant of some amount of doctrinal or behavioral differences (e.g. Romans 14 [8]). Now, it is also true that the Bible draws red lines, e.g. the Jesus-denying antichrists as previously mentioned, or those who preach a different gospel (Galatians 1:6–9 [9]). So there certainly are times when I think Christians should take a stand and say that some things are just plain wrong and dangerous—Jesus was not a moral or religious relativist, and the Bible is clear on many things. But, the idea that the institutional Church is this domineering thing, with inherent authority on all aspects of faith and morals, is very much not a universal Christian belief. (And, historically, a tremendous amount of evil has been done in the name of such a belief.)

Now, I readily admit that this doesn't quite defeat what you said, since you very well might define "the Church's line" to even include core theology like "Jesus is God". But to be honest, in general I think it's difficult to defend against accusations of the form "the Bible only says that you're for or against God for rhetorical reasons, to make it easier to convince people to agree with it". I certainly understand the argument, and I myself would apply it (or at least something vaguely like it) to other religions (e.g. how Jehovah's Witnesses shun those who leave). Still, I think the argument has the problem that it's unfalsifiable, at least when considered in a vacuum: If the Bible is false, then perhaps it makes sense that it would present itself as the exclusive way to God, but isn't that also the case if the Bible is true? Like, if Jesus really is "the way, the truth, and the life" and "no one comes to the Father except through" him (John 14:6), I'd certainly hope the Bible would go out of its way to tell everyone for their sake.

Some specific disagreements:

- "Proof trees" on Wikipedia redirects to the page for analytic tableaus, which I don't think is particularly relevant to Lean. I think natural deduction [1] would be infinitely more useful.

- Why is Gödel incompleteness necessary for one to understand how Lean works?

- Why is compactness necessary knowledge? In my experience, one can use and understand any modern proof assistant without knowing anything about model theory.