Fantasy rule of propositional logic in first order logic The fantasy rule in propositional logic is Fantasy Rule: If assuming $A$ to be a theorem leads to $B$ being a theorem, then $<A⊃B>$ is a theorem. An example is $$ \begin{align} &[\\\ & & &<p∧q> \tag{assumption}\\\ & & &p \tag{separation}\\\ & & &q \tag{separation}\\\ & & &<q∧p> \tag{joining}\\\ &]\\\ &<<p∧q>⊃<q∧p>> \tag{fantasy} \end{align} $$ How would I express the fantasy rule more formally using first or second order logic notation?

This is Conditional Introduction, or Conditional Proof, which is a well known principle in Propositional logic. First-order logic simply borrows this rule from propositional logic, so the rule is the same there.

There is no first-order logic description of this rule, since the rule is a rule _about_ logic statements (first-order logic statements, in the case of firs-order logic): it states how some logic staement can be derived from other logic statements or proof structures.

Thus, it is typically represented using text, or some kind of depiction, not unlike what you have:

| $\phi$ Assumption

| ...

| ...

| $\psi$

$\phi \rightarrow \psi \quad$ $\rightarrow \ $ Intro