Print the prenex normal form of a ZF formula that states `f:X->Y` using only AND, OR, IMPLIES, IN.

prenex-fxy.cc

/*

Copyright 2025 by Ji Luo

https://www.zhihu.com/question/11329797619/answer/95556221918

Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions:

The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software.

THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.

This code requires C++17 for sequencing of "operator,".

*/

#include<iostream>
#include<sstream>
#include<vector>
#include<cstdint>

enum quantifier_t { q_invalid, q_existential, q_universal };
char const * const quantifier_tex[] = { "\\undefined ", "\\exists ", "\\forall " };

struct prenex_t
{
  prenex_t()
  {
    *this, "(", f_X_Y_relational(), ")\\wedge(", f_X_somewhere(), ")\\wedge(", f_univocal(), ")";
  }
  friend std::ostream &operator<<(std::ostream &os, prenex_t const &that)
  {
    auto q_last = q_invalid;
    for (std::size_t i = 0; i != that.prefix.size(); )
    {
      auto const q_this = that.prefix[i++];
      if (q_this != q_last)
      {
        os << quantifier_tex[q_this];
        q_last = q_this;
      }
      if (i < 10)
      {
        os << "z_" << i;
      }
      else
      {
        os << "z_{" << i << "}";
      }
    }
    os << "(" << that.matrix.str() << ")";
    return os;
  }
private:
  std::size_t const forall()
  {
    prefix.push_back(q_universal);
    return prefix.size();
  }
  std::size_t const exists()
  {
    prefix.push_back(q_existential);
    return prefix.size();
  }
  prenex_t &operator,(char const *text)
  {
    matrix << text;
    return *this;
  }
  prenex_t &operator,(std::size_t const variable)
  {
    if (variable < 10)
    {
      matrix << "z_" << variable;
    }
    else
    {
      matrix << "z_{" << variable << "}";
    }
    return *this;
  }
  prenex_t &operator,(prenex_t &)
  {
    return *this;
  }
  // a = b
  prenex_t &extent(std::size_t const a, std::size_t const b)
  {
    // forall c:
    //   ((c in a) => (c in b)) &&
    //   ((c in b) => (c in a))
    auto const c = forall();
    return *this,
      "((", c, "\\in ", a, ")\\to(", c, "\\in ", b, "))\\wedge",
      "((", c, "\\in ", b, ")\\to(", c, "\\in ", a, "))";
  }
  // s = { e }
  prenex_t &pairing(std::size_t const s, std::size_t const e)
  {
    // forall t: (e in s) && ((t in s) => (t = e))
    auto const t = forall();
    return *this,
      "(", e, "\\in ", s, ")\\wedge((", t, "\\in ", s, ")\\to(", extent(t, e), "))";
  }
  // s = { a, b }
  prenex_t &pairing(std::size_t const s, std::size_t const a, std::size_t const b)
  {
    // forall t:
    //   (a in s) && (b in s) &&
    //   ((t in s) => ((t = a) || (t = b)))
    auto const t = forall();
    return *this,
      "(", a, "\\in ", s, ")\\wedge(", b, "\\in ", s, ")\\wedge",
      "((", t, "\\in ", s, ")\\to((", extent(t, a), ")\\vee(", extent(t, b), ")))";
  }
  // p = <a, b>
  prenex_t &kuratowski(std::size_t const p, std::size_t const a, std::size_t const b)
  {
    // forall c:
    //   ((c in p) => ((c = { a }) || (c = { a, b }))) &&
    //   ((c = { a }) => (c in p)) &&
    //   ((c = { a, b }) => (c in p))
    auto const c = forall();
    return *this,
      "((", c, "\\in ", p, ")\\to((", pairing(c, a), ")\\vee(", pairing(c, a, b), ")))\\wedge",
      "((", pairing(c, a), ")\\to(", c, "\\in ", p, "))\\wedge",
      "((", pairing(c, a, b), ")\\to(", c, "\\in ", p, "))";
  }
  prenex_t &f_X_Y_relational()
  {
    // forall p exists x y: (p in f) => ((x in X) && (y in Y) && (p = <x, y>))
    auto const p = forall();
    auto const x = exists();
    auto const y = exists();
    return *this,
      "(", p, "\\in f)\\to((", x, "\\in X)\\wedge(", y, "\\in Y)\\wedge(", kuratowski(p, x, y), "))";
  }
  prenex_t &f_X_somewhere()
  {
    // forall x exists y p: (x in X) => ((p = <x, y>) && (p in f))
    auto const x = forall();
    auto const y = exists();
    auto const p = exists();
    return *this,
      "(", x, "\\in X)\\to((", kuratowski(p, x, y), ")\\wedge(", p, "\\in f))";
  }
  prenex_t &f_univocal()
  {
    // forall x y1 y2 p1 p2: ((p1 = <x, y1>) && (p2 = <x, y2>) && (p1 in f) && (p2 in f)) => (y1 = y2)
    auto const x = forall();
    auto const y1 = forall();
    auto const y2 = forall();
    auto const p1 = forall();
    auto const p2 = forall();
    return *this,
      "((", kuratowski(p1, x, y1), ")\\wedge(", kuratowski(p2, x, y2), ")\\wedge(", p1, "\\in f)\\wedge(", p2, "\\in f))\\to(", extent(y1, y2), ")";
  }
private:
  std::vector<quantifier_t> prefix;
  std::stringstream matrix;
};

int main()
{
  std::cout <<
  "\\documentclass{article}\n"
  "\\begin{document}\n"
  "\\let\\IN\\in\n"
  "\\def\\in{\\IN\\nobreak}\n"
  "\\let\\ZZ z\n"
  "\\let\\LPAREN(\n"
  "\\catcode`\\z=13\n"
  "\\catcode`\\(=13\n"
  "\\def z_#1{\\ZZ_{#1}\\allowbreak}\n"
  "\\def({\\catcode`\\z=11\\relax\\catcode`\\(=12\\relax\\LPAREN}\n"
  "\\noindent$\n";
  std::cout << prenex_t{};
  std::cout <<
  "\n$\n\\end{document}\n";
  return 0;
}

/*

\documentclass{article}
\begin{document}
\let\IN\in
\def\in{\IN\nobreak}
\let\ZZ z
\let\LPAREN(
\catcode`\z=13
\catcode`\(=13
\def z_#1{\ZZ_{#1}\allowbreak}
\def({\catcode`\z=11\relax\catcode`\(=12\relax\LPAREN}
\noindent$
\forall z_1\exists z_2z_3\forall z_4z_5z_6z_7z_8z_9z_{10}z_{11}z_{12}z_{13}z_{14}z_{15}\exists z_{16}z_{17}\forall z_{18}z_{19}z_{20}z_{21}z_{22}z_{23}z_{24}z_{25}z_{26}z_{27}z_{28}z_{29}z_{30}z_{31}z_{32}z_{33}z_{34}z_{35}z_{36}z_{37}z_{38}z_{39}z_{40}z_{41}z_{42}z_{43}z_{44}z_{45}z_{46}z_{47}z_{48}z_{49}z_{50}z_{51}z_{52}z_{53}z_{54}z_{55}z_{56}(((z_1\in f)\to((z_2\in X)\wedge(z_3\in Y)\wedge(((z_4\in z_1)\to(((z_2\in z_4)\wedge((z_5\in z_4)\to(((z_6\in z_5)\to(z_6\in z_2))\wedge((z_6\in z_2)\to(z_6\in z_5)))))\vee((z_2\in z_4)\wedge(z_3\in z_4)\wedge((z_7\in z_4)\to((((z_8\in z_7)\to(z_8\in z_2))\wedge((z_8\in z_2)\to(z_8\in z_7)))\vee(((z_9\in z_7)\to(z_9\in z_3))\wedge((z_9\in z_3)\to(z_9\in z_7))))))))\wedge(((z_2\in z_4)\wedge((z_{10}\in z_4)\to(((z_{11}\in z_{10})\to(z_{11}\in z_2))\wedge((z_{11}\in z_2)\to(z_{11}\in z_{10})))))\to(z_4\in z_1))\wedge(((z_2\in z_4)\wedge(z_3\in z_4)\wedge((z_{12}\in z_4)\to((((z_{13}\in z_{12})\to(z_{13}\in z_2))\wedge((z_{13}\in z_2)\to(z_{13}\in z_{12})))\vee(((z_{14}\in z_{12})\to(z_{14}\in z_3))\wedge((z_{14}\in z_3)\to(z_{14}\in z_{12}))))))\to(z_4\in z_1)))))\wedge((z_{15}\in X)\to((((z_{18}\in z_{17})\to(((z_{15}\in z_{18})\wedge((z_{19}\in z_{18})\to(((z_{20}\in z_{19})\to(z_{20}\in z_{15}))\wedge((z_{20}\in z_{15})\to(z_{20}\in z_{19})))))\vee((z_{15}\in z_{18})\wedge(z_{16}\in z_{18})\wedge((z_{21}\in z_{18})\to((((z_{22}\in z_{21})\to(z_{22}\in z_{15}))\wedge((z_{22}\in z_{15})\to(z_{22}\in z_{21})))\vee(((z_{23}\in z_{21})\to(z_{23}\in z_{16}))\wedge((z_{23}\in z_{16})\to(z_{23}\in z_{21}))))))))\wedge(((z_{15}\in z_{18})\wedge((z_{24}\in z_{18})\to(((z_{25}\in z_{24})\to(z_{25}\in z_{15}))\wedge((z_{25}\in z_{15})\to(z_{25}\in z_{24})))))\to(z_{18}\in z_{17}))\wedge(((z_{15}\in z_{18})\wedge(z_{16}\in z_{18})\wedge((z_{26}\in z_{18})\to((((z_{27}\in z_{26})\to(z_{27}\in z_{15}))\wedge((z_{27}\in z_{15})\to(z_{27}\in z_{26})))\vee(((z_{28}\in z_{26})\to(z_{28}\in z_{16}))\wedge((z_{28}\in z_{16})\to(z_{28}\in z_{26}))))))\to(z_{18}\in z_{17})))\wedge(z_{17}\in f)))\wedge(((((z_{34}\in z_{32})\to(((z_{29}\in z_{34})\wedge((z_{35}\in z_{34})\to(((z_{36}\in z_{35})\to(z_{36}\in z_{29}))\wedge((z_{36}\in z_{29})\to(z_{36}\in z_{35})))))\vee((z_{29}\in z_{34})\wedge(z_{30}\in z_{34})\wedge((z_{37}\in z_{34})\to((((z_{38}\in z_{37})\to(z_{38}\in z_{29}))\wedge((z_{38}\in z_{29})\to(z_{38}\in z_{37})))\vee(((z_{39}\in z_{37})\to(z_{39}\in z_{30}))\wedge((z_{39}\in z_{30})\to(z_{39}\in z_{37}))))))))\wedge(((z_{29}\in z_{34})\wedge((z_{40}\in z_{34})\to(((z_{41}\in z_{40})\to(z_{41}\in z_{29}))\wedge((z_{41}\in z_{29})\to(z_{41}\in z_{40})))))\to(z_{34}\in z_{32}))\wedge(((z_{29}\in z_{34})\wedge(z_{30}\in z_{34})\wedge((z_{42}\in z_{34})\to((((z_{43}\in z_{42})\to(z_{43}\in z_{29}))\wedge((z_{43}\in z_{29})\to(z_{43}\in z_{42})))\vee(((z_{44}\in z_{42})\to(z_{44}\in z_{30}))\wedge((z_{44}\in z_{30})\to(z_{44}\in z_{42}))))))\to(z_{34}\in z_{32})))\wedge(((z_{45}\in z_{33})\to(((z_{29}\in z_{45})\wedge((z_{46}\in z_{45})\to(((z_{47}\in z_{46})\to(z_{47}\in z_{29}))\wedge((z_{47}\in z_{29})\to(z_{47}\in z_{46})))))\vee((z_{29}\in z_{45})\wedge(z_{31}\in z_{45})\wedge((z_{48}\in z_{45})\to((((z_{49}\in z_{48})\to(z_{49}\in z_{29}))\wedge((z_{49}\in z_{29})\to(z_{49}\in z_{48})))\vee(((z_{50}\in z_{48})\to(z_{50}\in z_{31}))\wedge((z_{50}\in z_{31})\to(z_{50}\in z_{48}))))))))\wedge(((z_{29}\in z_{45})\wedge((z_{51}\in z_{45})\to(((z_{52}\in z_{51})\to(z_{52}\in z_{29}))\wedge((z_{52}\in z_{29})\to(z_{52}\in z_{51})))))\to(z_{45}\in z_{33}))\wedge(((z_{29}\in z_{45})\wedge(z_{31}\in z_{45})\wedge((z_{53}\in z_{45})\to((((z_{54}\in z_{53})\to(z_{54}\in z_{29}))\wedge((z_{54}\in z_{29})\to(z_{54}\in z_{53})))\vee(((z_{55}\in z_{53})\to(z_{55}\in z_{31}))\wedge((z_{55}\in z_{31})\to(z_{55}\in z_{53}))))))\to(z_{45}\in z_{33})))\wedge(z_{32}\in f)\wedge(z_{33}\in f))\to(((z_{56}\in z_{30})\to(z_{56}\in z_{31}))\wedge((z_{56}\in z_{31})\to(z_{56}\in z_{30})))))
$
\end{document}

*/

prenex-fxy.png

prenex-fxy.tex

\documentclass{article}
\begin{document}
\let\IN\in
\def\in{\IN\nobreak}
\let\ZZ z
\let\LPAREN(
\catcode`\z=13
\catcode`\(=13
\def z_#1{\ZZ_{#1}\allowbreak}
\def({\catcode`\z=11\relax\catcode`\(=12\relax\LPAREN}
\noindent$
\forall z_1\exists z_2z_3\forall z_4z_5z_6z_7z_8z_9z_{10}z_{11}z_{12}z_{13}z_{14}z_{15}\exists z_{16}z_{17}\forall z_{18}z_{19}z_{20}z_{21}z_{22}z_{23}z_{24}z_{25}z_{26}z_{27}z_{28}z_{29}z_{30}z_{31}z_{32}z_{33}z_{34}z_{35}z_{36}z_{37}z_{38}z_{39}z_{40}z_{41}z_{42}z_{43}z_{44}z_{45}z_{46}z_{47}z_{48}z_{49}z_{50}z_{51}z_{52}z_{53}z_{54}z_{55}z_{56}(((z_1\in f)\to((z_2\in X)\wedge(z_3\in Y)\wedge(((z_4\in z_1)\to(((z_2\in z_4)\wedge((z_5\in z_4)\to(((z_6\in z_5)\to(z_6\in z_2))\wedge((z_6\in z_2)\to(z_6\in z_5)))))\vee((z_2\in z_4)\wedge(z_3\in z_4)\wedge((z_7\in z_4)\to((((z_8\in z_7)\to(z_8\in z_2))\wedge((z_8\in z_2)\to(z_8\in z_7)))\vee(((z_9\in z_7)\to(z_9\in z_3))\wedge((z_9\in z_3)\to(z_9\in z_7))))))))\wedge(((z_2\in z_4)\wedge((z_{10}\in z_4)\to(((z_{11}\in z_{10})\to(z_{11}\in z_2))\wedge((z_{11}\in z_2)\to(z_{11}\in z_{10})))))\to(z_4\in z_1))\wedge(((z_2\in z_4)\wedge(z_3\in z_4)\wedge((z_{12}\in z_4)\to((((z_{13}\in z_{12})\to(z_{13}\in z_2))\wedge((z_{13}\in z_2)\to(z_{13}\in z_{12})))\vee(((z_{14}\in z_{12})\to(z_{14}\in z_3))\wedge((z_{14}\in z_3)\to(z_{14}\in z_{12}))))))\to(z_4\in z_1)))))\wedge((z_{15}\in X)\to((((z_{18}\in z_{17})\to(((z_{15}\in z_{18})\wedge((z_{19}\in z_{18})\to(((z_{20}\in z_{19})\to(z_{20}\in z_{15}))\wedge((z_{20}\in z_{15})\to(z_{20}\in z_{19})))))\vee((z_{15}\in z_{18})\wedge(z_{16}\in z_{18})\wedge((z_{21}\in z_{18})\to((((z_{22}\in z_{21})\to(z_{22}\in z_{15}))\wedge((z_{22}\in z_{15})\to(z_{22}\in z_{21})))\vee(((z_{23}\in z_{21})\to(z_{23}\in z_{16}))\wedge((z_{23}\in z_{16})\to(z_{23}\in z_{21}))))))))\wedge(((z_{15}\in z_{18})\wedge((z_{24}\in z_{18})\to(((z_{25}\in z_{24})\to(z_{25}\in z_{15}))\wedge((z_{25}\in z_{15})\to(z_{25}\in z_{24})))))\to(z_{18}\in z_{17}))\wedge(((z_{15}\in z_{18})\wedge(z_{16}\in z_{18})\wedge((z_{26}\in z_{18})\to((((z_{27}\in z_{26})\to(z_{27}\in z_{15}))\wedge((z_{27}\in z_{15})\to(z_{27}\in z_{26})))\vee(((z_{28}\in z_{26})\to(z_{28}\in z_{16}))\wedge((z_{28}\in z_{16})\to(z_{28}\in z_{26}))))))\to(z_{18}\in z_{17})))\wedge(z_{17}\in f)))\wedge(((((z_{34}\in z_{32})\to(((z_{29}\in z_{34})\wedge((z_{35}\in z_{34})\to(((z_{36}\in z_{35})\to(z_{36}\in z_{29}))\wedge((z_{36}\in z_{29})\to(z_{36}\in z_{35})))))\vee((z_{29}\in z_{34})\wedge(z_{30}\in z_{34})\wedge((z_{37}\in z_{34})\to((((z_{38}\in z_{37})\to(z_{38}\in z_{29}))\wedge((z_{38}\in z_{29})\to(z_{38}\in z_{37})))\vee(((z_{39}\in z_{37})\to(z_{39}\in z_{30}))\wedge((z_{39}\in z_{30})\to(z_{39}\in z_{37}))))))))\wedge(((z_{29}\in z_{34})\wedge((z_{40}\in z_{34})\to(((z_{41}\in z_{40})\to(z_{41}\in z_{29}))\wedge((z_{41}\in z_{29})\to(z_{41}\in z_{40})))))\to(z_{34}\in z_{32}))\wedge(((z_{29}\in z_{34})\wedge(z_{30}\in z_{34})\wedge((z_{42}\in z_{34})\to((((z_{43}\in z_{42})\to(z_{43}\in z_{29}))\wedge((z_{43}\in z_{29})\to(z_{43}\in z_{42})))\vee(((z_{44}\in z_{42})\to(z_{44}\in z_{30}))\wedge((z_{44}\in z_{30})\to(z_{44}\in z_{42}))))))\to(z_{34}\in z_{32})))\wedge(((z_{45}\in z_{33})\to(((z_{29}\in z_{45})\wedge((z_{46}\in z_{45})\to(((z_{47}\in z_{46})\to(z_{47}\in z_{29}))\wedge((z_{47}\in z_{29})\to(z_{47}\in z_{46})))))\vee((z_{29}\in z_{45})\wedge(z_{31}\in z_{45})\wedge((z_{48}\in z_{45})\to((((z_{49}\in z_{48})\to(z_{49}\in z_{29}))\wedge((z_{49}\in z_{29})\to(z_{49}\in z_{48})))\vee(((z_{50}\in z_{48})\to(z_{50}\in z_{31}))\wedge((z_{50}\in z_{31})\to(z_{50}\in z_{48}))))))))\wedge(((z_{29}\in z_{45})\wedge((z_{51}\in z_{45})\to(((z_{52}\in z_{51})\to(z_{52}\in z_{29}))\wedge((z_{52}\in z_{29})\to(z_{52}\in z_{51})))))\to(z_{45}\in z_{33}))\wedge(((z_{29}\in z_{45})\wedge(z_{31}\in z_{45})\wedge((z_{53}\in z_{45})\to((((z_{54}\in z_{53})\to(z_{54}\in z_{29}))\wedge((z_{54}\in z_{29})\to(z_{54}\in z_{53})))\vee(((z_{55}\in z_{53})\to(z_{55}\in z_{31}))\wedge((z_{55}\in z_{31})\to(z_{55}\in z_{53}))))))\to(z_{45}\in z_{33})))\wedge(z_{32}\in f)\wedge(z_{33}\in f))\to(((z_{56}\in z_{30})\to(z_{56}\in z_{31}))\wedge((z_{56}\in z_{31})\to(z_{56}\in z_{30})))))
$
\end{document}