System of logic where "this statement is false" can be encoded?

Question

Is there a system of logic in which "this statement is false" can be encoded?

I'm familiar with the incompleteness theorems, so I know "this statement cannot be proven" can be expressed. If the system is consistent, then the statement is true but unprovable. However "this statement is false" evidently has no truth value. Is there a system of logic where such a statement can be encoded, and how is the statement analyzed? Does it depend on model theory?

Answer 1

Actually, I think any old programming language would work. You can write "this sentence is false" as a suitable divergent program, for instance let x :: Bool = not x in pseudo-Haskell code. (Recursive definitions are generally allowed in that language, for instance let x = 1:x gives an infinite list of 1's)

I'll go ahead and accept my own answer, unless anybody else happens to want to answer this.

Edit: There's a problem with this. Propositions-as-types lets you view programming languages as systems of (intuitionistic) logic, but the expression I gave is a term, not a type. I might delete this answer and write a new one, but let me work on this...