[dvt]

Any typing system that has at least two types (functional and non-functional) is a logic. In fact, modus ponens follows axiomatically via →elimination:

Let α → H be a functional type where α is a Person type, and H is a boolean type.

   Γ ⊢ α → H     Γ ⊢ α
  --------------------- (→e)
            Γ ⊢ H 

What this means is that you can have a function isAtHome(x) which takes a Person and returns a boolean. This schema itself is a logic insofar that it follows the same rules as the proposition A → B where A is true:

  A → B
  A
  ∴ B

(I wrote a simple and short paper[1] about typing λ-calculus in the context of Frege's concept horse paradox a few years ago.)

[1] http://dvt.name/logic/horse2.pdf

[chriswarbo]

Thanks, this is what I was getting at: the type systems of C++ and Java are logics in the sense of being formal syntactic systems with deduction rules.

I was struggling to think of a concrete example less trivial than function application, but I suppose my difficulty just shows how terrible these systems are when viewed as logics (but they're still logics!)

[dvt]

> Thanks, this is what I was getting at: the type systems of C++ and Java are logics in the sense of being formal syntactic systems with deduction rules.

Yep, exactly. Why I think it's hard to think of a more concrete example is because any type theory (like vanilla λ-calculus) is not deductive.

Let me clarify: once you add types to λ-calculus, it (amazingly) becomes deductive! But the type theory itself is not deductive (because types are not tractable, among other reasons).

[mafribe]

It's not enough for a formalism to exhibit modus ponens to be a logic. It also needs to be consistent.

[dvt]

There are many paraconsistent logics out there[1]. There are also many "trivial" logics out there[1] (which exhibit the Principle of Explosion). The former are useful, the latter not so much.

All them of them are logics. Consistency is not a requirement; it's simply a property a system may or may not have.

[1] http://plato.stanford.edu/entries/logic-paraconsistent/

[mafribe]

C++ and Java are not even paraconsistent: every type is inhabited.