How do you write the statement "Negation of a contradiction is a tautology" in predicate/ First Order logic?

Domain of discourse is propositions p(x) - x is a tautology q(x) - x is a contradiction (These were written by me)

So I want to state "Negation of a contradiction is a tautology" in FOL

Vx(¬q(x)→p(x)) This is what I've come up with, but the more I think about it this looks as "For all x, if x is not a contradiction then x is a tautology" which is not the same meaning as the question at hand

So how do I express the negation in this case?

Solution

You're quite right in your analysis. The statement you wrote says "anything that isn't a contradiction is a tautology". The issue here is you haven't defined what the negation of a proposition is, so there's no way to say "negation of a proposition" as a "noun". You can introduce a new non-logical function symbol (into your domain) to represent it. So we now have

P(x): an arity-1 predicate symbol, meaning "x is a tautology".
Q(x): an arity-1 predicate symbol, meaning "x is a contradiction".
N(x): an arity-1 function symbol, meaning "the negation of x".

And the formula is ∀x Q(x) -> P(N(x)): "any contradiction has its negation a tautology". Note how it's important to separate the "inner" and "outer" logic. The propositions you are reasoning about are just objects, and there's no particular reason for the "outer" ¬ to have much to do with the "inner" N. The new formula is in fact different from the original: I believe the original is very strong, and implies the inner logic is complete in the sense that every formula is either a contradiction or a tautology. The new one doesn't.