What is logic?

My take: it's a human means of systematically exploring implications of already accepted beliefs.

There are implicit and explicit forms of it.

The implicit form is something our brains do automatically and is a consequence of its structure. Perhaps the way it models things intrinsically does not allow for what we would call contradicting statements (though it contains many separate models which if unified would contain contradictions); then, the space of desirable implications is narrowed by a motivation to find a certain kind of implication (i.e. there is typically a goal when engaging in reasoning—we aren't often indifferently interested in all implications) combined with the fact that contradictions aren't allowed. It seems like implications are usually discovering that some entity belongs to a class it wasn't previously known to belong to, at which point it inherits the attributes of other things in that class.

The explicit forms seem like attempts to model the implicit form in mathematical language, in order to bring logical processes more under control of conscious thought, or 'executive function' (plus reasoning on paper extends working memory). It seems possible that with the 'correct' formulation, a logic could viewed as a theoretical science describing properties of the structure of the human brain that give rise to reasoning.

I don't think I would agree with the general statement that science gives us axioms. In normal usage, "axioms" are not the same as scientific "givens" or "data" even though it makes sense to interpret the word that way. In math and logic, the axioms we use are typically very foundational. We might say, "the empty set exists," or "for all x, it holds that x = x." There's no need to invoke science for these sorts of axioms and we can make many useful conclusions without it.

Part of the fun of logic is realizing that there are multiple forms of it which change one's language and ability to express ideas. They also don't dominate one another—some statements' truth depends upon what logic they're formalized within.

Model theory is good here in that it studies the connection between logical language and more "physical" models. Some of these models can give a relatable account for what a logic "means". For instance, Boolean logic correspond with set operations and therefore we can use that correspondence to portray a meaning for statements in Boolean-like logics.

Intuitionistic logic is an interesting one if you're not familiar with it. It can be seen as the logic of working with "demonstrations", building and analyzing them. For instance, if I have an object "X" such that witnessing it immediately convinces someone of the truth of "1+1=2", and if I have a whole collection of such items, then intuitionistic logic talks about how to compose and decompose collections of these things. Another interesting operation is "not" such that "not X" is a tool for using any X you happen to have to show that the world is inconsistent. This acts as a refutation of the existence of values like X!

This differs from set-like logics because, for instance, "not (not X)" is not the same as X: being able to show that if you had (a way to prove the world inconsistent if you had an X) you could show the world as inconsistent... it's a far cry away from actually having an X!

Intuitionistic logic is interesting for two reasons. First, it models communication and persuasion by being an algebra of "persuasive items" like X. Second, it's "constructive" and thus works similarly to how programming languages express things through their creation.

"Obviate" does not mean "make obvious", as I think was intended here. "To obviate" means "to remove (a need or difficulty)".

Gödel's arithmetization of logic is one hell of a beautiful mathematical idea, up there with linear algebra or probability theory. One of its big selling points for me was how easily it solves the unexpected hanging paradox. (The simplest arithmetization of the judge's self-referential statement is a statement about numbers that can be shown to be self-contradictory.) It's also cool how it turns Russell's paradox into Gödel's theorem, Curry's paradox into Löb's theorem, etc. The connections to algorithms and computability theory are also neat (Gödel's idea of "effectively axiomatized system" is any computer program that can print sentences, which has just the right amount of generality and connects to the halting problem in the obvious way). To me arithmetization is simply the right approach to logic, which easily subsumes everything that makes sense and rejects everything that doesn't.