gdy (nieformalnie) literalne wstawienie tego termu w rozważanej formule w miejscu któregoś z wolnych wystąpień zmiennej spowodowałoby związanie pewnej zmiennej termu ( w szczególności zmienne niebędące wolnymi w danej formule są wolne w niej dla wszystkich termów ← poprawić - to nie jest prawda).
Formalnie natomiast definiujemy to pojęcie indukcyjnie ze względu na budowę formuły następująco:
jeśli to jeśli jest formułą atomową, to jeśli to gdzie jeśli to
oraz jeśli to gdzie
Przykłady Rozważmy język ciał uporządkowanych Niech termami będą, odpowiednio oraz Rozważmy formułę Wówczas to term to term to formuła i podstawienie termu za zmienną w jest dopuszczalne, oraz są równokszałtne z przy czym podstawienie termu za zmienną jest niedopuszczalne (to jest jakaś bzdura - nie ma takiego pojęcia. Zmienna nie jest wolna dla tego termu w tej formule i dlatego podstawienie będzie nieskuteczne), zaś podstawienie tego samego termu za zmienną jest dopuszczalne (choć nieskuteczne), bowiem zmienna ta nie jest wolna w rozważanej formule.
Aksjomaty logiczne
Ta aksjomatyka jest od czapy (w szczególności jest niepełna) i sugeruję oprzeć się jednak na Pogorzelskim (r.