+++
title = "Double implication does not hold"
author = "Yann Herklotz"
tags = []
categories = []
backlinks = ["3a8g5e1"]
forwardlinks = ["3a8g5g", "3a8g5e3"]
zettelid = "3a8g5e2"
+++

However, one of the downsides of eliminating these variables from the
formulas means that the equivalence mentioned in the validation section
([\#3a8g5g]) does not hold anymore, and one can only really prove the
backward implication. However, maybe if the variables are also
eliminated for the formulas from the previous predicates, then an actual
equivalence can be shown between the two.

However, this equivalence might not be useful enough though. One of the
main problems faced with the predicates is that paths are completely
removed and some kind of proofs on the paths need to be reinstated. This
means that a lot of metadata needs to accompany the proof to show that
if one formula is true, then all the other formulas must be false. This
is the selection criteria for ɣ functions and therefore needs to hold.

  [\#3a8g5g]: /zettel/3a8g5g